Abstract
The question of how best to model and analyze systems with information security requirements has been of interest to the Rockwell Collins Advanced Technology Center since the beginning of the AAMP7G certification effort [Wilding et al. (in press) Design and verification of microprocessor systems for high-assurance applications]. Of particular interest are techniques that are amenable to automated formal reasoning, especially in a generic theorem proving or model checking context. In this chapter, we document research results that pertain to the GWV class of information flow theorems [Greve et al. (2003) Proceedings of ACL2’03; Greve et al. (2005) Proceedings of SSTC 2005]. We provide a mathematical underpinning for the theorems, explore some of their properties, demonstrate their application to selected examples, and describe their evolutionary history. We conclude by establishing a connection between our models of information flow and the classical notion of noninterference originally proposed by Goguen and Meseguer [Proceedings of the 1982 IEEE symposium on security and privacy (1982)].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alves-Foss J, Taylor C (2004) An analysis of the GWV security policy. In: Proceedings of the fifth international workshop on ACL2 and its applications, Austin, TX, Nov. 2004
Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT, Cambridge, MA
Goguen JA, Meseguer J (1982) Security policies and security models In: Proceedings of the 1982 IEEE symposium on security and privacy, pp 11–20. IEEE Computer Society Press, Washington, DC
Greve D (2004) Address enumeration and reasoning over linear address spaces. In: Proceedings of ACL2’04, Austin, TX, Nov. 2004
Greve D (2006) Parameterized congruences in ACL2. In: Proceedings of ACL2’06, Austin, TX, Nov. 2006
Greve D (2007) Scalable normalization of heap manipulating functions. In: Proceedings of ACL2’07, Austin, TX, Nov. 2007
Greve D, Wilding M, Vanfleet M (2003) A separation kernel formal security policy. In: Proceedings of ACL2’03
Greve D, Wilding M, Vanfleet M, Richards R (2005) Formalizing security policies for dynamic and distributed systems. In: Proceedings of SSTC 2005
Munoz C (2009) ProofLite product description. http://research.nianet.org/~munoz/ProofLite
Richards R (2010) Modeling and security analysis of a commercial real-time operating system kernel. In: Hardin D (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 301–322
Rushby J (1992) Noninterference, transitivity, and channel-control security policies. Technical report csl-92–2, SRI
Rushby J (2001) Formal verification of McMillan’s compositional assume-guarantee rule. Technical report, SRI, September 2001
Shannon C, Weaver W (1949) The mathematical theory of communication. University of Illinois Press, Champaign, IL
SRI, Incorporated (2009) PVS specification and verification system. http://pvs.csl.sri.com
Whalen M, Greve D, Wagner L (2010) Model checking information flow. In: Hardin D (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 381–428
Wilding M, Greve D, Richards R, Hardin D (2010) Formal verification of partition management for the AAMP7G microprocessor. In: Hardin D (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 175–191
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Greve, D.A. (2010). Information Security Modeling and Analysis. In: Hardin, D. (eds) Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, Boston, MA. https://doi.org/10.1007/978-1-4419-1539-9_9
Download citation
DOI: https://doi.org/10.1007/978-1-4419-1539-9_9
Published:
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-1538-2
Online ISBN: 978-1-4419-1539-9
eBook Packages: EngineeringEngineering (R0)