vRM: Verifying Reference Monitors via Exhaustive Access Pattern Generation
Abstract
Application sandboxes restrict program behavior to prevent system-wide damage. Within such sandboxes, reference monitors control which system calls are allowed based on predefined security policies. However, if an application is compromised, an attacker can issue complex and subtle sequences of system calls to try to bypass these protections, making it difficult to ensure that the reference monitor is fully secure.
In this project, we propose vRM (verified Reference Monitor), a verification framework that helps confirm the security of reference monitors. vRM automatically generates all possible system call access patterns using an SMT solver (Z3), then uses a concurrent model checker (CDSChecker) to test whether the reference monitor properly blocks any unauthorized access.
We demonstrate vRM’s effectiveness by focusing on a common type of vulnerability called TOCTTOU (Time-Of-Check to Time-Of-Use), which can occur during file access. We applied vRM to Apache 2.4.58 and successfully identified known TOCTTOU vulnerabilities in its reference monitor. We also formally verified a TOCTTOU-resistant algorithm as a positive case.
vRM provides a practical foundation for developing more secure sandbox environments in the future.
