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

• Applicant: Dr. Ulrich Schöpp
• Subject Area: Software Engineering and Programming Languages ; Theoretical Computer Science
• Term: from 2014 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 250888164

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.

• DFG Programme: Research Grants
• Co-Investigator: Dr. Steffen Jost