Proof-Carrying Hardware via Inductive Invariants

T. Isenberg, M. Platzner, H. Wehrheim, T. Wiersema, ACM Transactions on Design Automation of Electronic Systems (2017) 61:1--61:23.

Download
Restricted a61-isenberg.pdf 806.36 KB
Journal Article | English
Abstract
Proof-carrying hardware (PCH) is a principle for achieving safety for dynamically reconfigurable hardware systems. The producer of a hardware module spends huge effort when creating a proof for a safety policy. The proof is then transferred as a certificate together with the configuration bitstream to the consumer of the hardware module, who can quickly verify the given proof. Previous work utilized SAT solvers and resolution traces to set up a PCH technology and corresponding tool flows. In this article, we present a novel technology for PCH based on inductive invariants. For sequential circuits, our approach is fundamentally stronger than the previous SAT-based one since we avoid the limitations of bounded unrolling. We contrast our technology to existing ones and show that it fits into previously proposed tool flows. We conduct experiments with four categories of benchmark circuits and report consumer and producer runtime and peak memory consumption, as well as the size of the certificates and the distribution of the workload between producer and consumer. Experiments clearly show that our new induction-based technology is superior for sequential circuits, whereas the previous SAT-based technology is the better choice for combinational circuits.
Publishing Year
Journal Title
ACM Transactions on Design Automation of Electronic Systems
Issue
4
Page
61:1--61:23
LibreCat-ID
68

Cite this

Isenberg T, Platzner M, Wehrheim H, Wiersema T. Proof-Carrying Hardware via Inductive Invariants. ACM Transactions on Design Automation of Electronic Systems. 2017;(4):61:1--61:23. doi:10.1145/3054743
Isenberg, T., Platzner, M., Wehrheim, H., & Wiersema, T. (2017). Proof-Carrying Hardware via Inductive Invariants. ACM Transactions on Design Automation of Electronic Systems, (4), 61:1--61:23. https://doi.org/10.1145/3054743
@article{Isenberg_Platzner_Wehrheim_Wiersema_2017, title={Proof-Carrying Hardware via Inductive Invariants}, DOI={10.1145/3054743}, number={4}, journal={ACM Transactions on Design Automation of Electronic Systems}, publisher={ACM}, author={Isenberg, Tobias and Platzner, Marco and Wehrheim, Heike and Wiersema, Tobias}, year={2017}, pages={61:1--61:23} }
Isenberg, Tobias, Marco Platzner, Heike Wehrheim, and Tobias Wiersema. “Proof-Carrying Hardware via Inductive Invariants.” ACM Transactions on Design Automation of Electronic Systems, no. 4 (2017): 61:1--61:23. https://doi.org/10.1145/3054743.
T. Isenberg, M. Platzner, H. Wehrheim, and T. Wiersema, “Proof-Carrying Hardware via Inductive Invariants,” ACM Transactions on Design Automation of Electronic Systems, no. 4, pp. 61:1--61:23, 2017.
Isenberg, Tobias, et al. “Proof-Carrying Hardware via Inductive Invariants.” ACM Transactions on Design Automation of Electronic Systems, no. 4, ACM, 2017, pp. 61:1--61:23, doi:10.1145/3054743.
Main File(s)
File Name
a61-isenberg.pdf 806.36 KB
Access Level
Restricted Closed Access
Last Uploaded
2018-11-02T16:08:17Z


Export

Marked Publications

Open Data LibreCat

Search this title in

Google Scholar