Sciweavers

Share
SP
2010
IEEE

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

8 years 1 months ago
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...
Jason Franklin, Sagar Chaki, Anupam Datta, Arvind
Added 15 Feb 2011
Updated 15 Feb 2011
Type Journal
Year 2010
Where SP
Authors Jason Franklin, Sagar Chaki, Anupam Datta, Arvind Seshadri
Comments (0)
books