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

CT-T：安全嵌入式软件的资源引导实施

• 批准号: 0524059
• 负责人: Stephan Zdancewic
• 金额: $ 100万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2005
• 资助国家: 美国
• 起止时间: 2005-08-15 至 2010-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0524059&HistoricalAwards=false
• 关键词: CT; Resource; Guided; Implementation; Secure

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.

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