【V-SPELLS】DARPA加强对传统代码的理解，简化软件再造过程

国防和商业系统都充斥着难以现代化、增强和重新设计的传统软件，这主要是由于缺乏对底层老旧代码的有效理解，这使得预测修改的效果成为一项挑战。从国防的角度来看，人们越来越需要用更安全和更高性能的代码来增强或更换关键平台和系统中现有软件的组件，同时也希望在新硬件上使用传统软件来提高系统性能。然而，当在大型传统代码库中引入增强或替换措施时，新代码很可能无法安全地与系统的其余部分组合。现有的验证更新软件是按结构正确的方法关注于全新的软件开发，本质上限制了它们对从零开始开发的软件的有效性。此外，这些方法假定了现有的正式规范，通常对于传统系统不可用，并且它们需要某种形式的专业知识，而这是大多数开发人员都不容易找到的正式方法。

对此，国防高级研究计划局（DARPA）信息创新办公室（I2O）项目经理谢尔盖·布拉图斯（Sergey Bratus）表示：“为提高性能或安全性而对传统软件组件进行现代化改造面临很大风险，因为新软件尽管根据规范被验证是正确的，但将不能与现有基础设施完全兼容。系统所有者担心，他们可能需要对新代码进行多年的额外调整，才能与系统的实际行为可靠地进行互操作。”

为了应对这些挑战，DARPA推出了“大型传统软件的验证安全和性能增强”（Verified Security and Performance Enhancement of Large Legacy Software，V-SPELLS）项目，旨在使开发人员能够使用新的验证代码逐步增强现有的传统软件组件，并确保生成的软件能够安全地与现有系统组合。该方法的关键在于能够进行正确的增量更新，并通过构造兼容，而无需进行全新的软件开发或完全替换软件代码库。为了实现这一目标，V-SPELLS项目试图利用程序理解和验证中的新概念，以及领域特定语言（Domain Specific Languages，DSL）的最新发展，或者是专门用于特定应用领域的计算机语言，例如用于数据库查询的SQL或用于网络交换机的P4和路由器，以及大规模生产系统的可组合系统架构。

V-SPELLS项目的研究工作将集中在三个主要的探索技术领域。

第一个技术领域将探讨开发方法和工具，以创建迭代和交互方式理解大型传统代码库中的软件组件以及它们如何适应更大系统的情境的能力。为此，目标V-SPELLS工具将使开发人员能够半自动地从源代码中派生域结构和域逻辑的表示或表达式，如领域特定语言。在某些情况下，将传统代码提升或转换为领域特定语言可以将系统的性能提高一个数量级。V-SPELLS的目标是利用现有软件的传统代码库，并将其扩展和抽象为领域特定语言，在领域特定语言中可以安全、方便地修改。通过这种方法，V-SPELLS项目寻求将正式方法的能力和安全保证交给不是软件的正式验证专家的领域专家软件开发人员。

第二个技术领域将集中于为常规开发人员创建新的验证组件替换和增强功能，以安全地与系统的其余部分组合在一起。这包括创建一个集成环境，使开发人员能够结合领域特定语言和第一个技术领域的模型来重新实现、重新设计和增强系统的特定组件。

第三个技术领域将集中于开发流程、设计、标准和工具，以帮助克服前两个技术领域中创建的方法和工具所产生的任何性能降低或安全问题。这个研究领域还将探索如何确保对传统代码的增强，使之在现代硬件上运行。

来将通名&非诚勿扰

---

前情回顾

---

防务菌

---

有礼有节&百无禁忌