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 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 Cache and IO-Efficient Functional Algorithms

Presented as part of the 2013 HCSS conference.

ABSTRACT

file

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

Presented as part of the 2013 HCSS conference.

ABSTRACT

file

Visible to the public TrackOS: a Security-Aware RTOS

Presented as part of the 2013 HCSS conference.

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.