Seminar 2015-11-16: Professor Gene Tsudik - Scalable Embedded Device Attestation

Today, large numbers of smart interconnected devices providesafety and security critical services for energy grids, industrial controlsystems, building automation, transportation, and critical infrastructure. These devices often operate in groups, forming large, dynamic, and even self-organizing, networks. Collective integrity verification of software for device groups is necessary to ensure their correct and safe operation as well as to protect them against malware infestations. However, current device attestation schemes assume a single prover and do not scale to groups thereof. We discuss the design of SEDA -- the first attestation scheme for device groups. This work includes a formal security model for swarm attestation and two proof-of-concept SEDA implementations based on two recent attestation architectures for embedded systems. SEDA can efficiently attest device groups with dynamic or static topologies.

Rob van Glabbeek joins Royal Holland Society of Sciences and Humanities
2015-11-01 Rob van Glabbeek has been selected as a foreign member of the Royal Holland Society of Sciences and Humanities, a Dutch organisation founded in 1752 to to promote science in the broadest sense. Members are nominated by invitation only, based on their scientific achievements. So far 19 computer scientists have been awarded a membership

SYNTCOMP 2015
2015-10-30 Adam Walker wins the synthesis competition again this year in his category Sequential realizability More:

Seminar 2015-10-14: Nickolai Zeldovich - Using Crash Hoare Logic for Certifying the FSCQ File System

This talk will describe FSCQ, the first file system with a machine-checkable proof (using Coq) that its implementation meets its specification and whose specification includes crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.To state FSCQ's theorems, we introduce the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ running as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers.

2015-09-01 Google PhD fellowship
Congratulations to PhD student Qian Ge who has won a Google PhD fellowship with Research Proposal Title: Low Overhead Operating System Mechanisms for Eliminating Microarchitectural Timing Side Channels