![[HTTP Mutual Access Authentication]](/files/special/MutualAuth/index-en/mutual.png)
![[Fail-Safe C]](/files/project/FailSafeC-ja/FSC-logo.png){kind=logo}
![[Physical Analysis Attack on Cryptographic Module]](/special/SASEBO/SASEBO_banner_en.png)
![[LR-AKE]](/files/project/LRAKE-en/renew8.gif)
Research Team for Software Security
The weakest link of an information system often turns out to be its software. The reason is that software are too intricate and exposed: they rely on complicated hardware; malicious users can attack them using automatic tools, etc. In other words, they do not tolerate the approximations their complexity tends to introduce.
Actually, the flexibility and the vulnerability of information systems have the same origin: underlying software designs and programming languages are so rich that their complexity quickly leads to defects. Our approach is to provide rigorous means to enforce security requirements at all levels. Our research goes from the development of strong theoretical bases to the development of ready-to-use security tools for the end user.
Members
Leader
- Shibayama, Etsuya (Univ. Tokyo)
Research Scientists
- Affeldt, Reynald
- Artho, Cyrille
- Nowak, David
- Oiwa, Yutaka
- Suzaki, Kuniyasu
- Takagi, Hiromitsu
- Yamada, Kiyoshi
Post-Doctoral Fellow
- Nguyen, Quynh
- Tanaka, Miki
Associated Member
- Yonezawa, Akinori (Univ. Tokyo)
Research Topics
Software Security Enhancement
Given the large base of already-in-use software and Internet applications, it is important to provide means to enforce the security of existing information systems.
In order to check formally that a software is secure, one must first give a formal model of the software and its environment, and state formally what it means to be secure. We design formal languages for such purpose and algorithms to check security properties automatically.
For existing Internet applications, we provide automated analyses for well-known vulnerabilities (automatic check of cryptographic certificates, testing of Internet applications against models of well-known attacks, etc.). For low-level software, such as code written in assembly language, we develop logic-based verification techniques.
As new security problems appear everyday, software security cannot only be considered on a long-term basis. We thus provide a day-to-day survey of concrete vulnerabilities and quick means to fix security breaches. Based on this mundane experience, we provide guidelines for users and programmers to enforce security of existing information systems.
Secure Programming Environment
It is not only important to fix software security problems, but also to provide means to prevent them at the time of software development.
Low-level software such as code written in legacy C or assembly language come with many vulnerabilities inherited from their inherent complexity. In order to enhance the security of such applications, we provide mechanical solutions based on compilation techniques (fail-safe C compilation).
We aim at improving the traditional testing approach used in the industry by applying recent advances in formal verification to real-world programs, and developing ready-to-use extension to existing research formal tools (proof assistants, model checkers, type checkers, etc.).
We design original programming paradigms to enforce security checks and original programming languages that guarantee the absence of well-known security vulnerabilities (such as cross-site scripting and injection attacks).