"The nation's security and economy rely on infrastructures for communication, finance, energy distribution and transportation - all increasingly dependent on networked information systems. When these networked information systems perform badly or do not work at all, they put life, liberty and property at risk." —National Research Council, Trust in Cyberspace (F.B. Schneider, editor)

Cornell has one of the largest and most visible groups of security researchers found anywhere, tackling the fundamental problems of security and privacy in modern computing systems. Cornell has been a leader in computer security for decades, making widely recognized contributions that range from theoretical foundations to practical implementations to influence on government policy.

Cornell researchers are exploring the full space of security and privacy topics and working at at every level of the computing stack, with research on operating system and distributed system security, cryptography, language-based security, hardware-based security, network security, and security and privacy policies. We have a strong presence both in research that develops new methods for building secure computing systems and in research that identifies new kinds of security and privacy vulnerabilities. Security is a cross-cutting concern, and our work draws on the synergy with groups working on programming languages, operating systems, and logic and formal methods.


Foundational Cryptography Toolkit. We are building formal models and machine-checked proofs of security for cryptographic protocols. We are also trying to bridge the gap between these models and the actual code used to implement the protocols via program logics and certifying compilers. (Led by Greg Morrisett.)

CertiCoq. This project is building an open compiler for the functional language at the core of the Coq proof assistant. Our goal is to make it possible to write high-level code within Coq, prove its correctness, and then extract machine-executable code that is provably correct and performs well relative to other high-level programming languages. (Led by Greg Morrisett.)

Reactive Information Flow. Tags on information are an attractive alternative to putting guards on operations for enforcing security policies. But the language of tags must be expressive enough to allow new tags to be synthesized as values are produced during execution. Our work in RIF tags is aimed at satisfying the need. We are exploring them not only for enforcing confidentiality and integrity but also for supporting use-based privacy, which seems itself expressive enough to handle the various proposals people are advancing for what constitutes privacy in our digital age. (Led by Fred Schneider.)

Frenetic. Led by Nate Foster, this project is developing high-level languages for programming distributed collections of network switches. Frenetic makes it possible for developers to specify the behavior of an entire network using a single program that a compiler translates to low-level code that can be executed on each switch. This provides an exciting opportunity to enforce security, reliability, and performance guarantees using language-based techniques.

Bitcoin and Selfish Mining. Gün Sirer has been examining the incentives created by cryptocurrency systems and has shown that miners can collude to extract more than their fair share, undermining the stability of the system. He is now exploring how to make these systems more secure and scalable.

Nexus. Emin Gun Sirer and Fred B. Schneider are leading the development of Nexus, a new operating system for trusted computing. Nexus introduces new system abstractions, mechanisms and a novel system architecture for taking advantage of secure computing hardware. It enables users to leverage security guarantees of secure coprocessors without limiting flexibility and control over the local software configuration.

Fabric. In the Jif language, Andrew Myers pioneered adding security types to a real programming language. Jif is at the core of the Fabric system, which allows distributed systems to be programmed as though they run on a single computer, while enforcing information flow policies in an end-to-end fashion. Fabric nodes and programs from different and mutually distrusting security domains can securely share information, computation, and code. Jif was also used to develop Civitas, a secure voting system based on earlier work by Ari Juels. It is the first voting system implementation that allows voters to vote securely while provably providing universal verifiability, voter verifiability, anonymity, and coercion resistance.

Timing channels. Myers and Suh have recently been studying new methods for comprehensive control of timing channels at the operating system, hardware, and programming language levels. The technique of predictive mitigation provably controls how much information leaks via timing by making timing conform to predictions generated using only public information. Using a security-typed version of Verilog (SecVerilog), leaks can be prevented event through low-level hardware features such as cache.

Isis2. This project is exploring roles for security in scalable services for first tier of modern cloud computing data centers, where elasticity and rapid response have often been seen as more pressing needs than high assurance or security. Isis2 uses a variety of cryptographic tools to ensure that data replicated within such services cannot be stolen by applications sharing the same cloud that have gained the ability to spy on the network. The technology is packaged as an easily used software library which can be downloaded from Cornell under a BSD license and requires little more of the developer than the skills required to create an interactive GUI. Current research is focused on scalability and performance of the technology but, in the longer term, we want to expand our effort to explore high assurance for the "whole story" in cloud settings: the client platform, the Internet layer and the service within the cloud itself.

Security modeling. Joe Halpern is looking at logics that can deal with both qualitative and quantitative aspects of security. In addition, he is applying game theory to model aspects of security by extending standard solution concepts in game theory so that they can deal with faulty players and resource-bounded players. Halpern is also working on on getting clean, knowledge-based definitions of integrity and noninterference, even in the presence of declassification. Finally, he has been thinking about following up on work at CMU on applying ideas of causality (a topic he has been working on extensively) to auditing scenarios.

Synthesizing fault tolerance. Fault-tolerant distributed systems, algorithms, and protocols are notoriously hard to build. Going from a specification to an implementation involves many subtle steps that are easy to get wrong. Van Renesse and Schneider are using stepwise refinement to derive distributed algorithms from specification. Each step can be formally checked, and by making different design choices at each refinement step, diversity is introduced that can improve fault tolerance. Bickford, Constable, and Van Renesse are working to automate this process using NuPrl and are already able to synthesize a variety of executable consensus protocols.