“A framework for using standard typing algorithms incrementally – with applications to secure compilation.”
Modern languages are equipped with static type checking/inference that helps programmers to keep a clean programming style and to reduce errors. However, the ever-growing size of programs and their continuous evolution require building fast and efficient analysers. A promising solution is incrementality, aiming at only re-typing the diffs, i.e. those parts of the program that change or are inserted, rather than the entire codebase. We propose an algorithmic schema that drives an incremental usage of existing, standard typing algorithms with no changes.
We instantiated the algorithmic schema to many different languages and paradigms – including security type systems – with final the goal of checking the preservation of security properties upon program transformations.
Bibliograpy
- Conference papers
- Busi, Matteo, Pierpaolo Degano, and Letterio Galletta. “Robust Declassification by Incremental Typing.” Foundations of Security, Protocols, and Equational Reasoning. Springer, Cham, 2019. 54-69. [paper]
- Busi, Matteo, Pierpaolo Degano, and Letterio Galletta. “Using standard typing algorithms incrementally.” NASA Formal Methods Symposium. Springer, Cham, 2019. [paper] [extended version]
- Talks