Team for Research in
Ubiquitous Secure Technology

Citation
Jason Franklin. "Scalable Parametric Verification of Reference Monitors: How to Verify Reference Monitors without Worrying about Data Structure Size". Talk or presentation, 11, November, 2010.

Abstract
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 results of the paper are a set of small model theorems. These theorems state that in order to verify that a policy is enforced by a reference monitor with an arbitrarily large data structure, it is sufficient to model check the monitor with just one entry in its data structure. We apply our methodology to verify the designs of two hypervisors, SecVisor and the sHype mandatory-access-control extension to Xen. Our approach is able to prove that sHype and a variant of the original SecVisor design correctly enforces the expected security properties in the presence of powerful adversaries.

Electronic downloads

• 23%20-%20Franklin%20%28CMU%29.pptx · application/vnd.openxmlformats-officedocument.presentationml.pre · 152 kbytes

• HTML

  Jason Franklin. <a
  href="http://www.truststc.org/pubs/777.html"
  ><i>Scalable Parametric Verification of Reference
  Monitors: How to Verify Reference Monitors without Worrying
  about Data Structure Size</i></a>, Talk or
  presentation,  11, November, 2010.

• Plain text

  Jason Franklin. "Scalable Parametric Verification of
  Reference Monitors: How to Verify Reference Monitors without
  Worrying about Data Structure Size". Talk or
  presentation,  11, November, 2010.

• BibTeX

  @presentation{Franklin10_ScalableParametricVerificationOfReferenceMonitorsHow,
      author = {Jason Franklin},
      title = {Scalable Parametric Verification of Reference
                Monitors: How to Verify Reference Monitors without
                Worrying about Data Structure Size},
      day = {11},
      month = {November},
      year = {2010},
      abstract = {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
                results of the paper are a set of small model
                theorems. These theorems state that in order to
                verify that a policy is enforced by a reference
                monitor with an arbitrarily large data structure,
                it is sufficient to model check the monitor with
                just one entry in its data structure. We apply our
                methodology to verify the designs of two
                hypervisors, SecVisor and the sHype
                mandatory-access-control extension to Xen. Our
                approach is able to prove that sHype and a variant
                of the original SecVisor design correctly enforces
                the expected security properties in the presence
                of powerful adversaries.},
      URL = {http://www.truststc.org/pubs/777.html}
  }
  

Posted by Larry Rohrbough on 7 Dec 2010.
Groups: trust
For additional information, see the Publications FAQ or contact webmaster at www truststc org.