You are here

Research

	Multi Part Computation Goldwasser Models and protocols for securely computing on sensitive data held disjointly by different organizations to advance common goals.
	Future Internet Architecture Clark Assess the various NSF-funded proposals for a Future Internet, with special emphasis on security.
	Derailer Jackson Finding security holes in web applications by lightweight static analysis; eliminates need for explicit security policy by looking for anomalies in access control.
	Lattice-based Cryptography Vaikuntanathan Lattices are a new mathematical basis for cryptography that hold the promise to more efficient and more secure systems, that have so far resisted quantum attacks. We are interested both in building new types of cryptographic tools out of lattices, as well as in making basic constructions (such as private- and public-key encryption) ore efficient and light-weight.
	DOIDE Rinard Automatic discovery of errors in large applications. In combination with CodePhage, and TwoStep, enables the construction of an automatic error discovery and repair system that automatically uncovers and fixes errors before they appear in the wild.
	TwoStep Rinard Automatic repair of errors in large software systems via automatic patch generation techniques.
	CodePhage Rinard Automatic transfer of correct security checks between multiple applications, so that vulnerable applications automatically acquire secure code from other applications.
	SIFT Torralba Automatic detection and filtering of inputs that exploit security vulnerabilities. Provides a guarantee that no input that passes the filter can trigger certain vulnerabilities.
	The Ascend Secure Processor Devadas Outsourcing computation to the cloud has a difficult set of privacy challenges, a primary one being that the client cannot really trust cloud or application software. Encrypted computation achieves privacy by having the user specify encrypted inputs to a program in the cloud and returning encrypted results.Through innovations in architectural mechanisms, security protocols, and applied cryptography, we hope to show that it is viable to only trust hardware and not trust any software in some security-conscious applications, thereby substantially minimizing the trusted computing base for these applications.
	Program Obfuscation Vaikuntanathan Can we scramble (“obfuscate”) programs in such a way that they remain functional but their inner works are unintelligible to an adversary that tries to reverse-engineer it?
	Secure and dependable software by design Jackson Express security rules, extract evidence from designs, software, etc. to help designers analyze the system and find evidence that supports rules.
	Ur/Web Chlipala A programming language for web applications that rules out many security problems by construction.
	Bedrock Chlipala A platform for building software with strong security guarantees, via machine-checked mathematical proofs about assembly code; current focuses include deriving a correct and high-performance DNS server from a specification.
	Amber Zeldovich Kaashoek Developing a new approach to building web applications in which users directly control their own data, and can decide which applications are allowed to access what data, and with whom the data is shared.
	Keytree Zeldovich Kaashoek Designing a public-key infrastructure that provides nameto- key lookup with strong security properties in the face of a large number of nodes being compromised, using a form of consensus without server-to-server coordination.
	Secure OS kernels Zeldovich Kaashoek Developing OS kernels that can provide strong security guarantees, through the use of high-level languages like Go, or through formal proofs of correctness using a proof assistant like Coq.
	Proof-carrying Data Rivest Augment all messages in the system with proofs of how they were computed. This is composable. Each new computation incorporates the proofs that were attached to its inputs.
	Leakage-resilient Cyptography Goldwasser, Vaikuntanathan Can we build cryptographic systems that maintain security even if key information leaks continuously over time?
	Computing on Encrypted Data Goldwasser, Vaikuntanathan The theory and practice of processing data in encrypted form, and its applications in secure cloud computing. This includes design of powerful tools such as fully homomorphic encryption, functional encryption and protocols for secure multi-party computation.