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

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

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.