Gradual Security Typing for the Web
Raimil Cruz Concepción$^{1}$
$^{1}$Universidad de Chile. Santiago de Chile Chile
email: racruz@dcc.uchile.cl

Schedule:Thu 22st@10:45, Room: C

How to develop secure applications for the Web? Can we help programmers write applications that do not compromise privacy by leaking confidential information on public channels, either accidentally or due to malicious third-party code? Research in programming languages for security has explored two complementary approaches for controlling flow of sensitive data in programs: either statically, with a type system, or dynamically, with a runtime monitor. A static approach is preferable but might impose too much of a burden on programmers. Just like static and dynamic typing can be reconciled with a gradual type system, we propose to develop a gradual security type system, which allows programs to be partially typed, ensuring sound interoperability between the security typed and untyped fragments. Programmers can then start with a standard program, developed without security typing information, and progressively evolve their system towards a program with mixed static and dynamic guarantees. After addressing the language design issues involved in creating a practical secure gradually-typed language, we will extend Dart, a recent programming language for the Web developed by Google. Dart is a great target due to its increasing adoption for Web programming, and for its unique, highly pragmatic approach to type systems. The design and implementation of gradual security typing in Dart will be validated by securing existing Dart applications, and by studying how programmers use such a gradual type system.