Name
Abstract | ||
|---|---|---|
This paper presents UNDINE, a tool to automatically generate security critical Linear Temporal Logic (LTL) properties of processor architectures. UNDINE handles complex templates, such as those involving four or more variables, register equality to a constant, and terms written over register slices. We introduce the notion of event types, which allows us to reduce the complexity of the search for a given template. We build a library of nine typed property templates that capture the patterns that are common to security critical properties for RISC processors. We evaluate the performance and efficacy of UNDINE and our library of typed templates on the OR1200, Mor1kx, and RISC-V processors. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1109/MTV.2018.00013 | 2018 19th International Workshop on Microprocessor and SOC Test and Verification (MTV) |
Keywords | DocType | ISSN |
specification mining,type systems,linear temporal logic,processor security | Conference | 1550-4093 |
ISBN | Citations | PageRank |
978-1-5386-9251-6 | 0 | 0.34 |
References | Authors | |
19 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Calvin Deutschbein | 1 | 0 | 1.35 |
| Cynthia Sturton | 2 | 85 | 8.56 |