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

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

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.