Mining Hyperproperties from Behavioral Traces
| Autor: | Sujit Kumar Muduli, Mayank Rawat, Pramod Subramanyan |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
010302 applied physics
Very-large-scale integration Class (computer programming) Theoretical computer science Computer science Semantics (computer science) 02 engineering and technology Fuzz testing 01 natural sciences 020202 computer hardware & architecture Linear temporal logic 0103 physical sciences 0202 electrical engineering electronic engineering information engineering Information flow (information theory) Software system TRACE (psycholinguistics) |
| Zdroj: | VLSI-SOC |
| DOI: | 10.1109/vlsi-soc46417.2020.9344106 |
| Popis: | Many important specifications of hardware and software systems, such as secure information flow and determinism are expressible only as hyperproperties. In contrast to the well-studied class of trace properties, which specify sets of valid runs (aka traces) of a system, hyperproperties can specify relations that must hold between the traces of a system. While hyperproperties have many applications, primarily in security verification, coming up with hyperproperties for SoC validation is challenging. In this paper, we work toward addressing this challenge by introducing a framework for mining hyperproper-ties from execution traces of SoC designs. We introduce novel algorithms based on coverage-guided fuzzing that enable the generation of good input traces for the hyperproperty miner. We also present novel optimistic and pessimistic semantics for Hyper Linear Temporal Logic (HyperLTL) that enable principled evaluation of HyperLTL formulas over finite traces. Finally, we propose algorithms for scalably evaluating non-trivial satisfaction of candidate hyperproperties on sets of traces. Experiments on a small but realistic SoC design show the framework is effective in identifying useful hyperproperties. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|