Article Preview
Top1. Introduction
Multi-million gate system-on-chip (SoC) designs easily fit into today’s FPGAs. How to build a trustworthy computing system with high confidentiality of reconfigurable systems has been a broad research area for the past few years. Due to the ever increasing demand for higher speeds, lower memory and power requirements, it is increasingly difficult to transform a hardware description language (HDL) (Ghosh, 1999) into a bitstream format that can program the FPGA. This in turn increases the demand for the ability to verify security properties during the design transformation. To define and verify the system properties precisely in a program, formal methods play a key role. However, there are few works on the formal specification of hardware description languages and formal verification of security properties. This work presents a systematic approach to the problem that includes - a formal model of Handel C programs, security property specifications using linear temporal logic (LTL), and formal verification using a model checker. There are three steps. First, a Handel C program is formaly specified using Predicate Transition Nets. Second, the security properties – noninterference – are defined on the model description. Finally, the model and properties are converted into the model checker programming language and the properties are verified against the system (Figure 1).
Figure 1. Structure of security verification of reconfigurable systems
The main contributions of this paper are the modeling and specification of dynamic noninterference properties using Predicate Transition Nets (PrT Nets) and linear temporal logic (LTL) and formal verification of system properties on Handel C using a rewriting logic based model checker. This work establishes a platform for the formal verification and analysis of data flow security properties in Petri Nets using model checking.
The remainder of the paper is structured as follows. Section 2 presents background knowledge including FPGAs, Handel C, formal methods of Petri Nets and temporal logic, the dynamic semantics, security properties in FPGAs, and the principle of Maude, a model checker. Section 3 presents related works in formal verification using model checkers and discusses the limitations and benefits of existing verification tools. Section 4 introduces a PrT Net for Handel C programs based on an imperative Handel C syntax, defines the dynamic noninterference on the Handel C PrT Nets and the verification approach with meaningful results. Additionally a case study is used to validate the formal model and the results are discussed. Section 5 concludes the paper and presents future work.