Scalable Parametric Verification of Secure Systems: How to Verify Reference Monitors without Worrying about Data Structure Size

The security of systems such as operating systems, hypervisors, and web browsers depend critically on reference monitors to correctly enforce their desired security policy in the presence of adversaries. Recent progress in developing reference monitors with small code size and narrow interfaces has made automated formal verification of reference monitors a more tractable goal. However, a significant remaining factor for the complexity of automated verification is the size of the data structures (e.g., access control matrices) over which the programs operate. This paper develops a parametric verification technique that scales even when reference monitors and adversaries operate over unbounded, but finite data structures. Specifically, we develop a parametric guarded command language for modeling reference monitors and adversaries. We also present a parametric temporal specification logic for expressing security policies that the monitor is expected to enforce. The central technical res...

• Type: Journal
• Year: 2010
• Where: SP
• Authors: Jason Franklin, Sagar Chaki, Anupam Datta, Arvind Seshadri
• Keywords: Data Structure, Parametric Verification Technique, Reference Monitor, Security Privacy, SP 2010