Back to Search
Start Over
Formal Modeling and Verification of Security Property in Handel C Program
- Source :
- International Journal of Secure Software Engineering. 3:50-65
- Publication Year :
- 2012
- Publisher :
- IGI Global, 2012.
-
Abstract
- Multi-million gate system-on-chip (SoC) designs easily fit into today’s Field Programmable Gate Arrays (FPGAs). As FPGAs become more common in safety-critical and mission-critical systems, researchers and designers require information flow guarantees for the FPGAs. Tools for designing a secure system of chips (SOCs) using FPGAs and new techniques to manage and analyze the security properties precisely are desirable. In this work we propose a formal approach to model, analyze and verify a typical set of security properties – noninterference – of Handel C programs using Petri Nets and model checking. This paper presents a method to model Handel C programs using Predicate Transition Nets, a type of Petri Net, and define security properties on the model, plus a verification approach where security properties are checked. Three steps are used. First, a formal specification on the Handel C description using Petri Nets is extracted. Second, the dynamic noninterference properties with respect to the Handel C program statements are defined on the model. To assist in verification, a translation rule from the Petri Nets specification to the Maude programming language is also defined. Thus, the formal specification can be verified against the system properties using model checking. A case study of the pipeline multiplier is discussed to illustrate the concept and validate the approach.
Details
- ISSN :
- 19473044 and 19473036
- Volume :
- 3
- Database :
- OpenAIRE
- Journal :
- International Journal of Secure Software Engineering
- Accession number :
- edsair.doi...........1709747295bbec36eb9a0e5346c5e39a