CT-T: Resource-Guided Implementation of Secure Embedded Software

NSF 0524059安全嵌入式软件的资源引导实现Stephan Zdancewic，Rajeev Alur，Andre Scedrov该项目旨在促进网络嵌入式系统安全敏感软件的设计和实现的技术进步。该战略统一了两种可以为所需技术贡献关键要素的方法。第一种方法通过使用基于语言的信息流控制来为分布式系统提供安全性，这是一种用保密性和完整性要求来注释代码并使用这些要求来确定代码在网络系统中的必要位置的技术，该网络系统的特征是分布式代理之间的复杂信任关系。第二种方法是基于模型的设计，它以适用于可揭示设计错误的自动化分析技术的高抽象级别表达协议和系统，并提供自动化低级别平台特定细节的综合工具，从而减少编码错误。这种方法称为资源制导模型转换，允许设计者在高层次上表达系统及其安全需求，包括对目标平台的资源约束的注释。这项研究计划集中于开发基础理论和工具，以纠正和保留这些模型和协议的转换，促进安全分布式软件的综合。该项目通过使用Java Card技术实现安全交易系统来研究这种方法的有效性。

NSF 0524059Resource-guided Implementation of Secure Embedded SoftwareStephan Zdancewic, Rajeev Alur, Andre ScedrovThis project aims to advance the technology for designing andimplementing security-sensitive software for networked, embeddedsystems. The strategy unifies two approaches that can contribute keyelements to the needed technology. The first approach providessecurity for distributed systems by using language-based informationflow controls, a technique for annotating code with confidentiality andintegrity requirements and using these requirements to determine thenecessary placement of code in a networked system characterized bycomplex trust relations between distributed agents. The secondapproach, model-based design, expresses protocols and systems at ahigh level of abstraction suitable for automated analysis techniquesthat can reveal design errors, and provides synthesis tools thatautomate low-level platform-specific details, thereby reducing codingerrors. The approach, called resource guided modeltransformation, will allow the designer to express systems and theirsecurity requirements at a high level, including annotations forresource constraints of the target platform. This research programfocuses on the development of foundational theories and tools for correctnesspreserving transformations of these models and protocols, facilitatingthe synthesis of secure distributed software. The projectinvestigates the effectiveness of this methodology by implementingsecure transaction systems using Java Card technology.