Poster presentation at EuroSys 2024

A study on formal verification of reference monitors

Poster presentation at EuroSys 2024

Ryo Nakashima, a second-year master’s student (Information Physics & Computing) of Shinagawa Laboratory, gave a poster presentation at The European Conference on Computer Systems 2024 (EuroSys 2024), which was held in Greece in April 2024.

In this study, we aim to enhance the security of isolated execution environments such as sandboxes and TEEs through formal verification by concentrating on reference monitors, a central component of access control enforcement, in order to enable effective and realistic application of the formal verification approach.

As a first step, we aim to strengthen the reference monitors by a two-stage verification using automatic verification code generation and parallel verification to prevent Time-Of-Check-To-Time-Of-Use (TOCTTOU) attacks on the reference monitor.

Shinagawa Laboratory

Shinagawa Laboratory, The University of Tokyo