Team for Research in
Ubiquitous Secure Technology

Citation
"Scalable Parametric Verification of Secure Systems: How to Verify Reference Monitors without Worrying about Data Structure Size". J. Franklin, S. Chaki, A. Datta, A. Seshadri (eds.), 31st IEEE Symposium on Security and Privacy, May, 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 verifi- cation 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

• fcds-oakland2010.pdf · application/pdf · 244 kbytes

• HTML

   <a
  href="http://www.truststc.org/pubs/749.html"
  ><i>Scalable Parametric Verification of Secure
  Systems: How to Verify Reference Monitors without Worrying
  about Data Structure Size</i></a>, J. Franklin,
  S. Chaki, A. Datta, A. Seshadri (eds.), 31st IEEE Symposium
  on Security and Privacy, May, 2010.

• Plain text

   "Scalable Parametric Verification of Secure Systems:
  How to Verify Reference Monitors without Worrying about Data
  Structure Size". J. Franklin, S. Chaki, A. Datta, A.
  Seshadri (eds.), 31st IEEE Symposium on Security and
  Privacy, May, 2010.

• BibTeX

  @proceedings{FranklinChakiDattaSeshadri10_ScalableParametricVerificationOfSecureSystemsHowToVerify,
      title = {Scalable Parametric Verification of Secure
                Systems: How to Verify Reference Monitors without
                Worrying about Data Structure Size},
      editor = {J. Franklin, S. Chaki, A. Datta, A. Seshadri},
      organization = {31st IEEE Symposium on Security and Privacy},
      month = {May},
      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 verifi- cation
                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/749.html}
  }
  

Posted by Jessica Gamble on 5 May 2010.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.