Model Checking Information Flow

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.