CAREER: Removing the Human Element: Securing Deployed Cryptographic Systems through the use of Cryptographic Automation

密码学在日常生活中已经证明了其不可估量的价值，特别是随着越来越多的设备和交互正在向网络世界转移。 无论是浏览网页，进行购买，还是向朋友发送消息，密码学无处不在。 尽管用户（通常在不知不觉中）依赖于使用密码学的系统的安全性，但近年来在系统的密码部分中出现了许多严重的漏洞，其中一些具有很大的后果。 这些问题是由各种问题引起的，包括设计不佳、实现困难以及安全原语的使用（或误用）。 所有这些问题都有一个共同点：人的因素。 如果设计人员和软件工程师都有更好的工具来帮助他们在复杂的加密空间中导航，那么在分析这些不安全系统时发现的许多错误都可以避免。 密码自动化是一个相对较新且有前途的领域，旨在帮助解决其中许多问题，并使开发安全系统变得更容易，更不容易出错，即使对于非专家也是如此。 该项目的重点是从加密系统的部署和分析中消除人为因素。 通过使用加密自动化和开发工具，该项目的目标是更容易设计和安全地部署新的复杂加密系统，同时防止此类系统中出现不安全因素。 此外，该项目还包含一个教育计划，旨在帮助更广泛的受众更容易使用密码学。 中西部妇女计算机安全研讨会的创建，以及该项目的目标，不仅开发，而且还传播工具，将允许更多的学生，所有年龄段，更多的软件工程师，探索密码学和计算机安全，而不是被吓倒或害怕它。 该项目的核心围绕着构建工具的第一个推力，以帮助部署复杂的密码学。 这将主要侧重于自动化零知识证明代码的端到端开发，从表达证明语句到实现实现，以及匿名证书的其他应用程序。 第二个重点是在使用zkSNARKs（一种流行的零知识证明实例）的应用程序中自动发现加密漏洞。 这一突破将利用模糊技术来帮助程序员和最终用户检测现有的、已经部署的zkSNARK电路和应用程序中的不一致和错误。 第三个目标是通过各种动态分析和基于机器学习的方法的新颖组合，在传统和严重混淆的二进制文件中自动发现和识别现代密码算法和技术。 如果成功的话，这三个方面的结合，对于专家和非专家开发人员来说，使发现现有系统中密码学和潜在脆弱算法的使用变得更加容易，并设计和安全地部署新的复杂密码系统，同时防止这些不安全因素的发生。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的学术价值和更广泛的影响评审标准。

Cryptography has shown itself to be invaluable in everyday life, especially as more and more devices and interactions are moving to the online world. Whether it is browsing the web, making a purchase, or sending a message to a friend, cryptography is everywhere. Despite the fact that users (often unknowingly) rely on the security of systems that use cryptography, recent years have seen a number of serious vulnerabilities in the cryptographic pieces of systems, some with large consequences. These have been caused by various problems, including poor designs, difficulty of implementation, and use (or misuse) of (in)secure primitives. There is a common denominator in all of these problems: the human element. Many of the errors that are found when analyzing these insecure systems could have been prevented if both designers and software engineers had better tools to help them navigate the complex cryptographic space. Cryptographic automation is a relatively new and promising area that is designed to help solve many of these issues and make developing secure systems far easier and less error-prone, even for a non-expert. This project focuses on removing the human element from the deployment and analysis of cryptographic systems. Through the use of cryptographic automation and the development of tools, the project's aim is to make it easier to design and securely deploy new and complex cryptographic systems while preventing insecurities from occurring in such systems. Additionally, the project contains an education plan designed to help make cryptography more accessible to a broader audience. The creation of the Midwest Women in Computer Security Workshop, as well as the project's goal to not just develop but also disseminate tools, will allow more students of all ages, and more software engineers, to explore cryptography and computer security, instead of being intimidated or afraid of it.The project has three main thrusts. The core of the project centers around the first thrust of building tools to aid in the deployment of complex cryptography. This will principally focus on automating the end-to-end development of zero-knowledge proof code, from expressing the proof statement to realizing the implementation, with additional applications to anonymous credentials. The second thrust focuses on automating the discovery of cryptographic vulnerabilities in applications that use zkSNARKs, a popular zero-knowledge proof instantiation. This thrust will leverage fuzzing to help both programmers and end users detect inconsistencies and errors in existing, already deployed zkSNARK circuits and applications. The third thrust works to automate the discovery and identification of modern cryptographic algorithms and techniques in both traditional as well as heavily obfuscated binaries, through a novel combination of various dynamic analysis and machine-learning based approaches. If successful, the combination of these three thrusts will, for expert and non-expert developers alike, make it both easier to discover the use of cryptography and potentially vulnerable algorithms in existing systems as well as design and securely deploy new and complex cryptographic systems while preventing these insecurities from happening.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.