Name
Title | ||
|---|---|---|
Formal specification and verification of data separation in a separation kernel for an embedded system |
Abstract | ||
|---|---|---|
Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for verification. This paper describes a novel and practical approach to formally establishing the security of code. The approach begins with a well-defined set of security properties and, based on the properties, constructs a compact security model containing only information needed to rea-son about the properties. Our approach was formulated to provide evidence for a Common Criteria evaluation of an embedded soft-ware system which uses a separation kernel to enforce data separation. The paper describes 1) our approach to verifying the kernel code and 2) the artifacts used in the evaluation: a Top Level Specification (TLS) of the kernel behavior, a formal definition of dataseparation, a mechanized proof that the TLS enforces data separation, code annotated with pre- and postconditions and partitioned into three categories, and a formal demonstration that each category of code enforces data separation. Also presented is the formal argument that the code satisfies the TLS. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1145/1180405.1180448 | ACM Conference on Computer and Communications Security |
Keywords | Field | DocType |
data separation,practical approach,formal demonstration,formal specification,kernel code,security property,compact security model,formal definition,security protocol,formal argument,separation kernel,embedded system,formal verification,theorem proving,kernel functions,embedded software,software engineering,security model,computer access control,satisfiability | Programming language,Cryptographic protocol,Computer science,Formal specification,Theoretical computer science,Software,Common Criteria,Formal methods,Computer security model,Formal verification,Kernel (statistics) | Conference |
ISBN | Citations | PageRank |
1-59593-518-5 | 27 | 1.33 |
References | Authors | |
17 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Constance L. Heitmeyer | 1 | 898 | 151.71 |
| Myla Archer | 2 | 463 | 56.43 |
| Elizabeth I. Leonard | 3 | 110 | 8.48 |
| John McLean | 4 | 211 | 84.75 |