Type Systems for Secure Programming

CCR 9988491史密斯，斯科特约翰霍普金斯大学安全编程的类型系统由于代码的可移植性增加，语言设计中的安全性越来越受到关注。 大多数语言级别的安全机制都是语言设计之后才考虑的。 一个广为人知的语言安全系统是Java安全体系结构，可以在JDK 1.2中找到。 在那里，访问控制机制被编写为程序本身的代码，并且很难确定实际上有什么访问控制。 本研究的目标是开发一种面向程序设计语言的声明式安全体系结构。 在本计画中，我们将开发一个新的静态类型系统，以确保在执行阶段的安全性，其研究包含两个主要部分：一个新的静态类型系统，其中的安全资讯修饰程式类型（所谓的安全存取类型），以及适当的类型系统 * 一个新的模块系统，其中包括安全访问类型作为接口的一部分，并为此程序链接将需要验证安全属性。其目的是一个富有表现力的，灵活的安全纪律，允许静态验证，安全检查得到满足，允许运行时安全检查被避免。 属性的静态强制优于动态强制，这构成了编程语言设计和软件工程的基本支柱之一：类型本身作为程序行为的简明可读规范，并且缺少一类运行时错误，从而提供了更可靠的执行行为。 在安全编程的上下文中，“更可靠”直接转化为“更安全”。 这项研究的长期目标是建立一个更安全的互联网。

CCR 9988491Smith, ScottJohns Hopkins UniversityType Systems for Secure ProgrammingSecurity in language design is a rising concern due to increasedportability of code. Most language-level security mechanisms havebeen afterthoughts to language designs. One widely known languagesecurity system is the Java Security Architecture, found in the JDK1.2. There, access control mechanisms are written as code in theprogram itself, and it is difficult to determine what access controlsare actually in place. The goal of this research is to develop adeclarative security architecture for programming languages. In thisproject, a novel static type system for guaranteeing safety withrespect to certain security properties at run-time will be developed.The research consists of two main components,* a novel static type system in which security information decorates program types (so-called security access types), and the type system properly enforces propagation of this information;* a novel module system which includes security access types as part of the interface, and for which program linking will entail validating security properties.The aim is an expressive, flexible security discipline which allowsstatic verification that security checks are met, allowing run-timesecurity checks to be avoided. The advantages of static over dynamicenforcement of properties forms one of the basic pillars ofprogramming language design and software engineering: the typesthemselves serve as concise readable specifications of programbehavior, and the lack of a class of run-time errors gives morereliable execution behavior. In the context of secure programming,"more reliable" directly translates to "more secure". The long-termaim of this research is a more secure internet.