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

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

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.