Advanced cryptographic technology can enable new kinds of computing systems: secure computing and storage in the cloud, internet voting systems, secure cryptographic currencies, and more. Unfortunately, advanced cryptography has not been widely adopted, because it tends to be too complex for most software developers to use correctly. Even experts make security-critical mistakes with modern cryptography. The expected outcome of this project is a simpler and less error-prone way to build computer systems that use advanced cryptography. This project explores a new way to put the full power of cryptography in the hands of programmers. Programmers will not design cryptography directly. Instead, they will develop software using a high-level programming language, and the Viaduct system will automatically introduce sophisticated cryptographic mechanisms as needed to make the software secure. Viaduct automatically compiles high-level protocols to primitive cryptographic building blocks, offering formal security guarantees in the form of machine-checkable security proofs. The project demonstrates end-to-end synthesis based on universal composability as a practical way to build secure systems. Viaduct will make security engineering stronger, easier, and cheaper. The project will open-source Viaduct and promote it through demos, workshops, and tutorials.
SaTC: CORE: Large: Viaduct: A Framework for Automatically Synthesizing Cryptographic Protocols