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 Taming JavaScript with F*

ABSTRACT:

Traditionally confined to the web browser, JavaScript can now be found on servers running Node.js, on mobile devices of all sorts, and even natively in the Windows 8 operating system. Developers for these platforms routinely program directly in JavaScript, although, increasingly, they may generate JavaScript from other sources using a variety of compilers. Despite this widespread adoption, the programming languages community has a dubious view of JavaScript, because its unusual semantics can lead to hard-to-detect bugs.

file

Visible to the public Verifying the Trusted Platform Module

ABSTRACT

As the hardware root-of-trust for trusted computing systems, the Trusted Platform Module (TPM) is critical in establishing system trust. The TPM 1.2 and associated Trusted Software Stack (TSS) are described by 700 pages of precise, textual documentation and have not been formally modeled or verified. As the hardware root of trust for trusted computing, formal treatment of the TPM is warranted. To address assurance issues in the TPM, we are developing and verifying a model of the TPM 1.2 using PVS.