Abstract
Information flow modeling describes how information can be transferred between different locations within a software and/or hardware system. In this chapter, we define a notion of information flow based on traces that is useful for describing flow relations for synchronous dataflow languages such as SimulinkⓇ (The Mathworks, Inc.) and SCADE™ (Esterel Technologies, Inc.) that are often used for hardware/software codesign. We then define an automated method for analyzing information flow properties of Simulink models using model checking. This method is based on creating a flow model that tracks information flow throughout the model. Often, information flow properties are defined in terms of some form of noninterference, which states informally that objects in one security domain cannot perceive the actions of objects within another domain. We demonstrate that this method preserves the GWV functional notion of noninterference. We then describe how this proof relates to the GWV theorem and provide some insight into the relationship of the flow model and the flow graphs used in GWVr1. Finally, we demonstrate our analysis technique by analyzing the architecture of the Turnstile high-assurance cross-domain guard platform using our Gryphon translation framework and the Prover™ model checker.
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
Bensalem S, Caspi P, Parent-Vigouroux C, Dumas C (1999) A methodology for proving control systems with Lustre and PVS. In: Proceedings of the seventh working conference on dependable computing for critical applications (DCCA 7), San Jose, January 1999
Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT, Cambridge, MA
Colaço JL, Girault A, Hamon G, Pouzet M (2004) Towards a higher-order synchronous data-flow language. In ACM fourth international conference on embedded software (EMSOFT’04), Pisa, Italy, September 2004
Esterel Technologies, Inc. SCADE Suite product description. http://www.esterel-technologies.com/products/scade-suite
Goguen JA, Meseguer J (1982) Security policies and security models. In: Proceedings of the 1982 IEEE symposium on security and privacy. IEEE Computer Society Press, Washington, DC, pp 11–20
Greve D (2010) Information security modeling and analysis. In: Hardin D (ed) Design and verification of microprocessor systems for high-assurance applications. Springer, Berlin, pp 249–299
Halbwachs N, Caspi P, Raymond P, Pilaud D (1991) The Synchronous dataflow programming language lustre. Proc IEEE 79(9):1305–1320
IRST http://nusmv.irst.itc.it/ The NuSMV model checker, IRST, Trento, Italy
Le Guernic P, Gautier T, Borgne ML, Maire CL (1991) Programming real-time applications with signal. Proc IEEE 79:1321–1336
MacLean J (1992) Proving noninterference and functional correctness using traces. J Comput Secur 1:37–57
The Mathworks, Inc., Simulink and stateflow product description. http://www.mathworks.com/Simulink, http://www.mathworks.com/products/stateflow/
McMillan K (1998) Verification of an implementation of Tomasulo’s algorithm by compositional model checking. In: Proceedings of the tenth international conference on computer aided verification (CAV’98) Vancouver, Canada, June 1998
McMillan K (1999) Circular compositional reasoning about liveness. In: Advances in hardware design and verification: IFIP WG10.5 international conference on correct hardware design and verification methods (CHARME’99), pp 342–345
Munoz C (2009) ProofLite product description. http://research.nianet.org/~munoz/ProofLite
Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: 11th International conference on automated deduction (CADE), vol 607, Saratoga, NY, June 1992, pp 748–752
Prover Technologies, Inc. Prover SL/DE plug-in product description. http://www.prover.com/products/prover_plugin
Reactive Systems, Inc. Reactis product description. http://www.reactive-systems.com
Rockwell Collins Turnstile Product Page. http://www.rockwellcollins.com/products/gov/airborne/cross-platform/information-assurance/cross-domain-solutions/index.html
Roscoe AW, Goldsmith MH (1999) What is intransitive noninterference? In: Proceedings of the 12th IEEE computer security foundations workshop, pp 228–238
Rushby J (1992) Noninterference, transitivity, and channel-control security policies. Technical report csl-92–2, SRI
Ryan PYA (1991) A CSP formulation of non-interference. In: Cipher. IEEE Computer Society Press, Washington, DC, pp 19–27
SRI, Incorporated. PVS specification and verification system. http://pvs.csl.sri.com
SRI, SAL home page. http://www.csl.sri.com/projects/sal/
Whalen M, Cofer D, Miller S, Krogh B, Storm W (2007) Integration of formal analysis into a model-based software development process. In: 12th International workshop on industrial critical systems (FMICS 2007), Berlin, Germany, July 2007
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
Whalen, M.W., Greve, D.A., Wagner, L.G. (2010). Model Checking Information Flow. 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_13
Download citation
DOI: https://doi.org/10.1007/978-1-4419-1539-9_13
Published:
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-1538-2
Online ISBN: 978-1-4419-1539-9
eBook Packages: EngineeringEngineering (R0)