Enforcing and analysing programming guidelines for secure web programming with type systems

使用类型系统执行和分析安全 Web 编程的编程指南

• 批准号: 250888164
• 负责人: Dr. Ulrich Schöpp
• 金额: --
• 依托单位: fortiss GmbH -Landesforschungsinstitut des Freistaats Bayern für softwareintensive Systeme
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2014
• 资助国家: 德国
• 起止时间: 2013-12-31 至 2022-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/250888164?language=en
• 关键词: Enforcing; analysing; programming; guidelines; secure

Modern software typically must be able to interact with the whole world. While until recently such worldwide interaction was quite rare now almost any business software has a web interface allowing anyone to interact with the software be it only by entering a wrong password. One can therefore no longer rely on high skill and experience of specialist programmers; almost anyone writes web software exposed to worldwide security threats. To address this issue programming guidelines and "best practices" have been developed, see e.g. www.owasp.org, that summarise and condense the expert Knowledge and make it available to a larger community. Whether or not such programming guidelines are applied and whether they have been correctly applied, is however left to the good will of the programmers. In this project we want to develop automatic methods based on type systems that are capable of checking that programmingguidelines have been correctly and reasonable applied without compromising the flexibility of writing code. Besides further developing type system methodology this also requires us to devise a formalism in which to rigorously define such policies which typically are given in plain English and by examples. In order that users will actually trust the system and perceive it as a useful tool it will be necessary to achieve a rather high degree of accuracy. For example, if an already sanitized user input is stored in a string buffer and later on read out it is not necessary to re-sanitize it. If the system does not recognize such a situation users will neglect its warnings in the future. This requires the use, combination, and further development of cutting-edge developments in program analysis, model checking and type systems. In order to guarantee appropriate feedback to the user and to achieve seamless integration we will use type-theoretic formulations of These methods resulting then in a single customizable type system capable ofenforcing a large span of guidelines for secure web programming.A running example will be the security threat posed by code injection where a malicious user inputs strings containing code fragments that (assuming a corresponding vulnerability at the server's side) may potentially be executed. Further examples come form industrial contacts and web portals like OWASP and SANS. The main scientific innovation is the focus on Guidelines rather than vulnerabilities and the development of a freely configurable type system.

现代软件通常必须能够与整个世界进行交互。 虽然直到最近这种全球性的互动是相当罕见的，但现在几乎所有的商业软件都有一个Web界面，允许任何人与软件进行交互，只要输入错误的密码。因此，人们不能再依赖于专业程序员的高技能和经验;几乎所有人都编写了暴露于全球安全威胁的Web软件。为了解决这个问题，已经开发了编程指南和“最佳实践”，参见例如www.owasp.org，其总结和浓缩了专家知识并将其提供给更大的社区。然而，这些程序设计准则是否得到应用以及它们是否得到正确应用，则取决于程序设计人员的良好意愿。在这个项目中，我们希望开发基于类型系统的自动方法，这些方法能够检查编程指南是否正确和合理地应用，而不会影响编写代码的灵活性。除了进一步发展类型系统方法，这也需要我们设计一个形式主义，在其中严格定义这些政策，通常是在平原英语和例子。为了使用户真正信任该系统，并将其视为一个有用的工具，有必要达到相当高的准确度。例如，如果一个已经清理过的用户输入被存储在字符串缓冲区中，然后被读出，那么就没有必要重新清理它。如果系统没有识别出这种情况，用户将来就会忽略它的警告。 这就需要使用、结合和进一步发展程序分析、模型检查和类型系统方面的前沿发展。为了保证给用户提供适当的反馈并实现无缝集成，我们将使用这些方法的类型理论公式，从而产生一个能够强制执行安全Web编程的大范围指导方针的单个可定制类型系统。（假设在服务器侧存在相应的漏洞）可能会被执行。进一步的例子来自行业联系人和门户网站，如OWASP和SANS。主要的科学创新是专注于指导方针而不是脆弱性，并开发了一个可自由配置的类型系统。