CPS: Medium: Secure Smart Machining

加工是软件。Gcode是用于铣床、车床和等离子切割机等加工工具的编程语言，开发于20世纪50年代末，至今仍是主导语言。在过去的60年里，编程语言和软件发生了巨大的变化和进步，但Gcode基本保持不变。对于遗留系统和新系统（如3D打印机）都是如此。机械加工是网络物理系统的先驱，但从计算的角度来看，它仍然是半个世纪以前的事情。使机床成为现代化的网络化编程系统有可能彻底改变价值400亿美元的机械加工行业。该研究项目将展示使用新的嵌入式操作系统、程序分析、安全代码分发和用户工具安全可靠地提高加工自动化的新技术。该研究依赖于三个重要原则：离散化、可编程安全性和端到端审计完整性。第一个原理，离散化，是一种极大地简化正确性检查和验证不变量的程序表示方法。而不是依靠隐式曲线和几何来定义物理形状，程序使用由所需的加工精度定义的显式离散表示。第二个原则是可编程安全性，通过使用即使整个系统崩溃也能正常运行的高保证软件，使快速变化的软件具有与传统加工系统相同的物理安全性。最后，端到端完整性和审计允许操作人员在运行代码之前验证代码，并允许系统证明程序正确执行。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Machining is software. Gcode, the programming language for machining tools such as milling machines, lathes, and plasma cutters, was developed in the late 1950s and remains the dominant language today. In the past 60 years, programming languages and software have changed and advanced tremendously, but Gcode remains mostly unchanged. This is true both for legacy systems as well as new ones, such as 3D printers. Machining pioneered cyber-physical systems but, from a computing perspective, remains half a century in the past. Enabling machine tools as modern, networked programming systems has the potential to revolutionize the $40B machining industry.This research project will demonstrate new techniques that safely and securely improve machining automation, using new embedded operating systems, program analysis, secure code distribution, and user tools. The research relies on three important principles: discretization, programmable safety, and end-to-end integrity with auditing. The first principle, discretization, is a method of program representation that greatly simplifies correctness checks and verifying invariants. Rather than rely on implicit curves and geometric to define physical shapes, programs use an explicit, discretized representation defined by the desired machining precision. The second principle, programmable safety, allows quickly-changing software to have the same physical safety as traditional machining systems, by using high-assurance software that operates correctly even if the entire system crashes. Finally, end-to-end integrity and auditing allows operators to verify code before running it and allows the system to prove that programs executed correctly.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.