Language-based Security for VHDL | Terkel K. Tolstrup
| | Abstract | The need for reliable performance of computerised systems is well-known, yet the security verification of hardware systems is often none-existing or applied in an ad-hoc manner. To overcome this issue, standards such as the Common Criteria has been successful in listing points of attention for a thorough investigation of a system. Hence in this thesis it is investigated how language-based security techniques can be adapted and applied to hardware specifications. The focus of the investigation is on the information flow security that is required by the standard. Information flow security provides a strong notion of end-to-end security in computing systems. However sometimes the policies for information flow security are limited in their expressive power, and this complicates the matter of specifying policies even for simple systems. These limitations often become apparent in contexts where confidential information is released under specific conditions.
This thesis presents a novel policy language for expressing permissible information flow using expressive constraints on the execution traces for programs. Based on the policy language a security property is proposed and shown to be a generalised intransitive non-interference condition. The security property is defined on a fragment of the hardware description language VHDL that is suitable for implementing the Advanced Encryption Standard algorithm.
The means to verify the property is provided in the terms of a static information flow analysis. The goal of the analysis is to identify the entire information flow through the VHDL program. The result of the analysis is presented as a nontransitive directed graph that connects those nodes (representing either variables or signals) where an information flow might occur. The approach is compared to traditional approaches and shown to allow for a greater precision.
Practical implementations of embedded systems are vulnerable to side channel attacks. In particular timing channels have had a great impact on the security verification of algorithms for cryptography. In order to address this another security property stating the absence of timing channels is presented. Again, verification is provided by a static analysis, that identifies the timing behaviour of a program. This analysis consists of a type system that identifies the delay between when a value enters the system and when it leaves it again. Programs accepted by our analysis are shown to have no timing channels. | | Type | Ph.D. thesis [Academic thesis] | | Year | 2007 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-PHD-2007-174 | | Note | Supervised by Prof. Flemming Nielson, and Prof. Hanne Riis Nielson, IMM, DTU. | | Electronic version(s) | [pdf] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|