Formal Modeling and Verification of Security Property in Handel C Program

2012 ◽  
Vol 3 (3) ◽  
pp. 50-65
Author(s):  
Yujian Fu ◽  
Jeffery Kulick ◽  
Lok K. Yan ◽  
Steven Drager
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Formal Specification ◽  
Critical Systems ◽  
Formal Approach ◽  
C Programs ◽  
Translation Rule ◽  
Security Properties ◽  
C Program ◽  
Security Property

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.

scholarly journals Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking

2020 ◽  
Vol E103.D (3) ◽  
pp. 702-705
Author(s):  
Nao IGAWA ◽  
Tomoyuki YOKOGAWA ◽  
Sousuke AMASAKI ◽  
Masafumi KONDO ◽  
Yoichiro SATO ◽  
...  
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Symbolic Representation ◽  
Bounded Model Checking ◽  
Time Petri Nets ◽  
Representation Of Time
Sign in / Sign up

Export Citation Format

Share Document