Taxonomic Search: Harvard University

7 results

Results

file

Visible to the public Verified Software-Based Fault Isolation

Submitted by Katie Dey on Tue, 05/14/2013 - 1:09pm. Contributors:

ABSTRACT

Native Client (NaCL) is a new service provided by Google's Chrome for directly executing native binary code in the context of the browser.  The security of NaCL depends upon a binary checker that is meant to enforce a basic sandbox policy known as software-based fault isolation.  Recently, we built a new binary checker for NaCL and verified its correctness using the Coq proof assistant: If the checker says "yes" on a binary, and the binary is loaded into a suitable context, then the binary is guaranteed to respect the sandbox.

file

Visible to the public Re-Education of Injured Nervous Systems: Infant Spontaneous Kicking Study

Submitted by Katie Dey on Fri, 11/04/2011 - 1:20pm. Contributors:

NSF Project: Programmable Second Skin for Re-Educating Injured Nervous Systems

Abstract 2

See also: http://cps-vo.org/node/1813

file

Visible to the public Augustinian and Manichaean Science

Submitted by Katie Dey on Mon, 12/03/2012 - 11:43am. Contributor:

Peter Louis Galison is the Pellegrino University Professor in History of Science and of Physics at

page

Visible to the public Integrating Programming Language and Operating System Information Security Mechanisms

Submitted by Katie Dey on Sun, 10/21/2012 - 8:03pm

The interaction between language-based security mechanisms and operating system security mechanisms has remained largely unexamined, and unexploited.  Language-based information security uses programming language abstractions and techniques to reason about and enforce information security, and can provide strong fine-grained application-specific information security guarantees.