HW/SW (HCSS'13)

file

Visible to the public Above and Beyond: seL4 Noninterference and Binary Verification (PT. 1)

ABSTRACT:

In 2009, the L4.verified project completed the world's first verification of functional correctness for a general-purpose OS kernel [2], seL4. Functional correctness here was embodied by a formal theorem of refinement, which stated that the behavior of the C code that implemented the kernel accorded with an abstract specification of how the kernel was meant to function.

file

Visible to the public Verification of X86 Binary-Level Programs

ABSTRACT

Verification of binary programs is required to assure their correct execution. However, correctness verification of binary programs often involves significant user expertise and time-consuming manual effort. We present an approach for automatically verifying some x86 binary programs using symbolic execution on a formal model of the x86 instruction set architecture. Our approach can reduce the work involved in the proof development process by automating the verification of program fragments and sometimes even complete subroutines.

file

Visible to the public Verification of Concurrent Software in the Context of Weak Memory

ABSTRACT

Multiprocessors are now so widespread that verification cannot ignore any longer the flavor of concurrency that they implement. Contrary to what most formal verification works assume, the execution model for concurrent programs is not Lamport's Sequential Consistency (SC), where an execution of a program corresponds to an interleaving of the instructions of the program.

file

Visible to the public Verification of Concurrent Software in the Context of Weak Memory

ABSTRACT

Multiprocessors are now so widespread that verification cannot ignore any longer the flavor of concurrency that they implement. Contrary to what most formal verification works assume, the execution model for concurrent programs is not Lamport's Sequential Consistency (SC), where an execution of a program corresponds to an interleaving of the instructions of the program.

file

Visible to the public Applying Language-Based Static Verification in an ARM Operating System

ABSTRACT

In recent years, we have seen a proliferation of small, embedded, electronic devices controlled by computer processors as powerful as the ARM(r). These devices are now responsible for tasks as varied as flying a plane, talking on a cellphone, or helping to perform surgery. Some of these tasks have severe consequences for a mistake caused by faulty programming or missed deadlines. The best defense against these mistakes is to prevent them from happening in the first place.

file

Visible to the public TrackOS: a Security-Aware RTOS

ABSTRACT

Cyber-physical systems (CPS) are becoming an increasingly attractive target for adversaries to launch software attacks against. New approaches are needed to detect software-based vulnerabilities while meeting the constraints of embedded execution in CPS.