Sustainable Integrity (HCSS'15)

file

Visible to the public Bringing Hardware Hacking to Life

Abstract:

But is it practical? This question is always banded about to dismiss some research publication showing an advanced attack such as side-channel power analysis or glitching. Most of these publications are using university-backed labs or expensive commercial equipment, leading to the assumption an attacker wouldalso require such equipment.

file

Visible to the public A Formal Specification of x86 Memory Management

Abstract:

We are developing a formal and executable x86 ISA specification that includes memory management via paging and segmentation. We regularly use this specification to mechanically verify user-level x86 machine-code programs. Our recent efforts have been devoted to developing a theory for reasoning about system-level programs that are aware of memory management mechanisms like paging.

file

Visible to the public Language-based Hardware Verification with ReWire: Just Say No! to Semantic Archaeology

Abstract:

There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers.

file

Visible to the public Biologically Inspired Software Defenses

Abstract:

Today's software monoculture creates asymmetric threats. An attacker needs to find only one way in, while defenders need to guard a lot of ground. Adversaries can fully debug and perfect their attacks on their own computers, exactly replicating the environment that they will later be targeting.

file

Visible to the public Remote Attestation for Cloud-Based Systems

Abstract:

Remote attestation provides a mechanism for gathering information from remote systems for assessing their trustworthiness. Using remote attestation an appraiser needing to assess trustworthiness makes a request to gather information from a target. The target's attestation manager responds by executing an attestation protocol that gathers and bundles evidence that is sent to the appraiser. The appraiser un-bundles evidence and uses primary evidence to assess the target and meta-evidence to assess the target's attestation process.

file

Visible to the public Detecting Malice in Commodity Software

Abstract:

The U.S. Government and commercial industry depend on commodity software. Unfortunately, the long supply chain that produces this software provides many opportunities for adversaries to insert backdoors or other hidden malicious functionality along the way. How can we gain confidence that our commodity software is free of malice? Conventional wisdom holds that this problem is so fundamentally difficult that no practical solution is attainable.