NDLI: Verifying hyperproperties of hardware systems

Please wait, while we are loading the content...

Formal verification for computer security: lessons learned and future directions

Understanding evolution through algorithms

Network verification: when Clarke meets Cerf

Machine learning and systems for the next frontier in formal verification

Verifying hyperproperties of hardware systems

A paradigm shift in verification methodology

Program synthesis for networks

The FMCAD 2016 graduate student forum

Soundness of the quasi-synchronous abstraction

Synthesizing adaptive test strategies from temporal logic specifications

Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakening

Extracting behaviour from an executable instruction set model

Categorical semantics of digital circuits

Equivalence checking by logic relaxation

Minimal unsatisfiable core extraction for SMT

Efficient uninterpreted function abstraction and refinement for word-level model checking

Optimizing horn solvers for network repair

On ∃ ∀ ∃! solving: a case study on automated synthesis of magic card tricks

Property-directed k-induction

Lazy proofs for DPLL(T)-based SMT solvers

Verifiable hierarchical protocols with network invariants on parametric systems

Modular specification and verification of a cache-coherent interface

Proof certificates for SMT-based model checkers for infinite-state systems

Routing under constraints

A consistency checker for memory subsystem traces

Hybrid partial order reduction with under-approximate dynamic points-to and determinacy information

Formal verification of division and square root implementations, an Oracle report

Integrating proxy theories and numeric model lifting for floating-point arithmetic

Trustworthy specifications of ARM® v8-A and v8-M system level architecture

Equivalence checking using Gröbner bases

Accurate ICP-based floating-point reasoning

Swapper: a framework for automatic generation of formula simplifiers based on conditional rewrite rules

Lazy sequentialization for TSO and PSO via shared memory abstractions

Combining requirement mining, software model checking and simulation-based verification for industrial automotive systems

Verifying hyperproperties of hardware systems

Content Provider	ACM Digital Library
Author	Finkbeiner, Bernd Rabe, Markus
Abstract	This tutorial presents hardware verification techniques for hyperproperties. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable. Such a comparison cannot be represented as a set of traces and thus falls outside the standard notion of trace properties. A comparison between execution traces can, however, be represented as a set of sets of traces, which is called a hyperproperty. Hyperproperties occur naturally in many applications beyond their origins in security: examples include the symmetric access to critical resources in distributed protocols and Hamming distances between code words in coding theory. The hardware verification approach of the tutorial is based on recently developed temporal logics for hyperproperties. Unlike classic temporal logics like LTL or CTL, which refer to one computation path at a time, temporal logics for hyperproperties like HyperLTL and HyperCTL can express properties that relate multiple traces by explicitly quantifying over multiple computation paths simultaneously. We will relate the logics to the linear-branching spectrum of process equivalences, and show that even though the satisfiability problem of the logics is undecidable in general, the model checking problem can be solved efficiently. We will show how the logics can be used to verify real hardware designs, including an I2C bus master, the symmetric access to a shared resource in a mutual exclusion protocol, and the functional correctness of encoders and decoders for error resistant codes.
Starting Page	5
Ending Page	5
Page Count	1
ISBN	9780983567868
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2016-10-03
Publisher Place	Austin
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

On Verifying Timed Hyperproperties

On Verifying Timed Hyperproperties

Monitoring hyperproperties

Verifying Global Neural Network Specifications using Hyperproperties

Introducing Asynchronicity to Probabilistic Hyperproperties

Verification of Quantitative Hyperproperties Using Trace Enumeration Relations

The State Evolution Method for Verifying Hardware Systems

Verifying Hardening Techniques for Distributed Electronic Systems in Critical Applications

Specifying and verifying hardware for tamper-resistant software

Verifying hyperproperties of hardware systems

Similar Documents

On Verifying Timed Hyperproperties

On Verifying Timed Hyperproperties

Monitoring hyperproperties

Verifying Global Neural Network Specifications using Hyperproperties

Introducing Asynchronicity to Probabilistic Hyperproperties

Verification of Quantitative Hyperproperties Using Trace Enumeration Relations

The State Evolution Method for Verifying Hardware Systems

Verifying Hardening Techniques for Distributed Electronic Systems in Critical Applications

Specifying and verifying hardware for tamper-resistant software

Verifying hyperproperties of hardware systems