CAREER: Programming Languages for Reliable and Secure Low-level Systems

许多关键系统，包括操作系统、嵌入式系统和通信系统，都是低级的。 也就是说，它们需要对硬件资源进行仔细控制，以实现所需的功能并表现良好。 低级软件越来越普遍，因此它必须是可靠和安全的，但其日益增加的复杂性使得这样做变得相当困难。本项目致力于开发，实施，应用和评估编程语言技术，以确保低级系统的安全性和可靠性。 该方法是采用新的静态分析技术，主要是新的类型检查和推理系统，用于自动检查低级软件常见的习惯用法的正确使用。这些习惯用法包括手动内存管理、并发和动态重新配置;它们的不正确使用可能导致服务失败、数据损坏和安全漏洞。 为了进行评估，新技术正在被纳入一种名为Cyclone的新的类C编程语言中，然后用于构建或移植真实的低级软件，包括设备驱动程序、网络数据包处理器和服务器以及嵌入式控制软件。 这些系统与传统开发的系统进行了实验比较，以评估其灵活性，可用性和性能。这项工作将导致新的工具和方法来构建更可靠和安全的低级别系统。 通过在真实的底层软件上验证这些技术，它们将具有很强的相关性和影响力。 所有结果将在公共论坛（会议和期刊）上发表，并作为研究生和本科教育的一部分。 所有开发的软件都将免费提供，并可供工业和教育领域的非专家使用。

Many critical systems, including operating systems, embedded systems, and communications systems, are low-level. That is, they require careful control over hardware resources to implement needed functionality and to perform well. Low-level software is increasingly common, so it must be reliable and secure, but its increasing complexity makes doing so quite difficult.This project is working to develop, implement, apply, and evaluate programming language technologies to ensure the security and reliability of low-level systems. The approach is to employ novel static analysis techniques, mostly novel type checking and inference systems, for automatically checking proper usage of idioms common to low-level software. These idioms include manual memory management, concurrency, and dynamic reconfiguration; their incorrect usage can lead to service failures, data corruption, and security exploits. For assessment, the new techniques are being incorporated into a new C-like programming language called Cyclone, which is then used to build or port real low-level software, including device drivers, network packet processors and servers, and embedded control software. These systems are experimentally compared against traditionally-developed systems to evaluate their flexibility, usability, and performance.This work will result in new tools and methodologies for building more reliable and secure low-level systems. By validating these techniques on real low-level software, they will have strong relevance and impact. All results will be presented in public forums (conferences and journals) and as part of graduate and undergraduate education. All developed software will be freely available, and usable to non-experts in industry and education.