Model Checking Information Flow

  • Michael W. Whalen
  • David A. Greve
  • Lucas G. Wagner
Chapter

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.

Keywords

Sugar U_Read Propa Nonin Glean 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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 1999Google Scholar
  2. 2.
    Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT, Cambridge, MAGoogle Scholar
  3. 3.
    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 2004Google Scholar
  4. 4.
    Esterel Technologies, Inc. SCADE Suite product description. http://www.esterel-technologies.com/products/scade-suite
  5. 5.
    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–20Google Scholar
  6. 6.
    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–299CrossRefGoogle Scholar
  7. 7.
    Halbwachs N, Caspi P, Raymond P, Pilaud D (1991) The Synchronous dataflow programming language lustre. Proc IEEE 79(9):1305–1320CrossRefGoogle Scholar
  8. 8.
    IRST http://nusmv.irst.itc.it/ The NuSMV model checker, IRST, Trento, Italy
  9. 9.
    Le Guernic P, Gautier T, Borgne ML, Maire CL (1991) Programming real-time applications with signal. Proc IEEE 79:1321–1336CrossRefGoogle Scholar
  10. 10.
    MacLean J (1992) Proving noninterference and functional correctness using traces. J Comput Secur 1:37–57Google Scholar
  11. 11.
    The Mathworks, Inc., Simulink and stateflow product description. http://www.mathworks.com/Simulink, http://www.mathworks.com/products/stateflow/
  12. 12.
    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 1998Google Scholar
  13. 13.
    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–345Google Scholar
  14. 14.
    Munoz C (2009) ProofLite product description. http://research.nianet.org/~munoz/ProofLite
  15. 15.
    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–752Google Scholar
  16. 16.
    Prover Technologies, Inc. Prover SL/DE plug-in product description. http://www.prover.com/products/prover_plugin
  17. 17.
    Reactive Systems, Inc. Reactis product description. http://www.reactive-systems.com
  18. 18.
  19. 19.
    Roscoe AW, Goldsmith MH (1999) What is intransitive noninterference? In: Proceedings of the 12th IEEE computer security foundations workshop, pp 228–238Google Scholar
  20. 20.
    Rushby J (1992) Noninterference, transitivity, and channel-control security policies. Technical report csl-92–2, SRIGoogle Scholar
  21. 21.
    Ryan PYA (1991) A CSP formulation of non-interference. In: Cipher. IEEE Computer Society Press, Washington, DC, pp 19–27Google Scholar
  22. 22.
    SRI, Incorporated. PVS specification and verification system. http://pvs.csl.sri.com
  23. 23.
  24. 24.
    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 2007Google Scholar
  25. 25.
    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–191CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  • Michael W. Whalen
    • 1
  • David A. Greve
  • Lucas G. Wagner
  1. 1.Rockwell Collins, Inc.BloomingtonUSA

Personalised recommendations