Securing the Internet presents great challenges and research opportunities. Potential applications such as Internet voting, universally available medical records, and ubiquitous e-commerce are all being hindered because of serious security and privacy concerns. The epidemic of hacker attacks on personal computers and web sites only highlights the inherent vulnerability of the current computer and network infrastructure.
Adequately addressing security and privacy concerns requires a combination of technical, social, and legal approaches. Topics currently under active investigation in the department include mathematical modeling of security properties, implementation and application of cryptographic protocols, secure and privacy-preserving distributed algorithms, trust management, verification of security properties, and proof-carrying code. There is also interest in the legal aspects of security, privacy, and intellectual property, both within the department and in the world-famous Yale Law school, with which we cooperate. Some of these topics are described in greater detail below.
Joan Feigenbaum has conducted direction-setting research on various aspects of cryptography, security, and privacy for more than thirty years. For example, she was the co-founder (with Matt Blaze and Jack Lacy) of the security-research area of “trust management.” In 2020, Blaze, Feigenbaum, and Lacy won the IEEE Symposium on Security and Privacy Test-of-Time Award for their 1996 paper “Decentralized Trust Management.” Currently, Professor Feigenbaum is working on “socio-technical” issues in the interplay of computer science and law, including the tension between strong encryption and lawful surveillance.
Ben Fisch will start at Yale in 2022 as co-director of the Yale Applied Cryptography Laboratory and Assistant Professor of Computer Science. He is broadly interested in problems related to privacy and verifiability in information systems, with a special attention on applications of cryptography to blockchains. He has worked closely with the blockchain industry, and his research has impacted open source projects including Filecoin, Ethereum, and Chia. His research has focused on various types of cryptographic proof systems, including zero-knowledge proofs, proofs of storage, proofs of correct computation, and verifiable delay functions.
Michael Fischer is interested in security problems connected with Internet voting, and more generally in trust and security in multiparty computations. He has been developing an artificial society in which trust has a precise algorithmic meaning. In this setting, trust can be learned and used for decision making. Better decisions lead to greater social success. This framework allows for the development and analysis of some very simple algorithms for learning and utilizing trust that are easily implementable in a variety of settings and are arguably similar to what people commonly use in everyday life.
Charalampos Papamanthou is the co-director of the Yale Applied Cryptography Laboratory and an Associate Professor of Computer Science at Yale. Before Yale, he was the Director of the Maryland Cybersecurity Center (MC2) and an Associate Professor of Electrical and Computer Engineering at the University of Maryland, College Park, where he joined in 2013 after a postdoc at UC Berkeley. He works on applied cryptography and computer security—and especially on technologies, systems and theory for secure and private cloud computing. He has received the NSF CAREER award, the Google Faculty Research Award, the Yahoo! Faculty Research Engagement Award, the NetApp Faculty Fellowship, the UMD Invention of the Year Award, the Jimmy Lin Award for Invention, the George Corcoran Award for Excellence in Teaching and was also finalist for the 2020 Facebook Privacy Research award. His research has been funded by federal agencies (NSF, NIST and NSA) and by the industry (Google, Yahoo!, NetApp, VMware, Amazon, Ergo, Ethereum and Protocol Labs). His PhD is in Computer Science from Brown University (2011) and he also holds an MSc in Computer Science from the University of Crete (2005), where he was a member of ICS-FORTH. His work has received over 9,000 citations and he has published in venues and journals spanning theoretical and applied cryptography, systems and database security, graph algorithms and visualization and operations research.
Zhong Shao leads the FLINT group at Yale, which is applying formal methods to complex security-sensitive systems in such a way that they can guarantee to users that these systems really are trustworthy. There are several challenges standing in the way of achieving this goal. One challenge is how to specify the desired security policy of a complex system. In the real world, pure noninterference is too strong to be useful. It is crucial to support more lenient security policies that allow for certain well-specified information flows between users, such as explicit declassifications. A second challenge is that real-world systems are usually written in low-level languages like C and assembly, but these languages are traditionally difficult to reason about. A third challenge is how to actually go about conducting a security proof over low-level code and then link everything together into a system-wide guarantee.
He and his team are developing a new set of formal techniques and tools for overcoming all of these challenges. They are developing a new methodology for formally specifying, proving, and propagating information-flow security policies using a single unifying mechanism, called the “observation function.” A policy is specified in terms of an expressive generalization of classical noninterference, proved using a general method that subsumes both security-label proofs and information-hiding proofs, and propagated across layers of abstraction using a special kind of simulation that is guaranteed to preserve security. To demonstrate the effectiveness of the new methodology, they are building an actual end-to-end security proof, fully formalized and machine-checked in the Coq proof assistant, of a nontrivial concurrent operating system.
Anurag Khandelwal is interested in building cloud-based systems that are secure by construction. His team is currently exploring the design of secure storage systems, where simply storing the data in an encrypted form is insufﬁcient to ensure security: an adversary can launch powerful attacks that use data access patterns to learn damaging information about the data. Existing countermeasures against these attacks remain impractical at the scale of modern storage systems due to large bandwidth and/or storage overheads. His team is exploring how modeling access to the storage as a statistical distribution can enable significantly more scalable solutions that still retain formal security guarantees against practical adversarial settings.
Lin Zhong and his team are interested in the security and privacy of application data in the context of personal and cloud computing. Modern systems often assume the operating system as part of the trusted computing base and as a result, modern operating systems by design have unfettered access to application data. His team is exploring both incremental changes to existing operating systems, e.g., Linux, and clean-slate operating system designs to decouple virtualization, the essential role of operating systems, from data access. They are also exploring the use of machine learning, especially adversarial learning, to minimize privacy-sensitive information in data collected on mobile and IoT devices.