Static and dynamic enforcement of security via relational reasoning

Abstract

Static analysis is an important building block of security, as it allow us to guarantee that formal security properties will be preserved during any possible execution of a system, before it is even deployed. Many of the most interesting security properties can only be formulated in a relational setting, i.e., by comparing multiple executions. Due to limitations of existing tools, many of these properties can only be verified manually. However, manual verification of such properties is infeasible on a large scale, as it is a cumbersome task requiring a high degree of expert knowledge. We hence in this thesis present novel verification frameworks, that enable an automated analysis of such relational security properties. We base all of these frameworks on type systems, resulting in efficient and modular approaches. We present novel type systems for the verification of strong relational security properties in the area of cryptographic protocols and web security and study relational reasoning in a theorem prover. We first propose a framework for the verification of observational equivalence in cryptographic protocols and establish automated proofs for protocols that previously could not be covered by automated tools. We then propose a runtime monitor for web browsers, a form of a dynamic type system, parametrized by simple declarative policies. We design a set of constraints for these policies that is sufficient to guarantee strong web session confidentiality and integrity properties. We also propose a type system for web application code in a formal model of the web, that enforces a strong notion of web session integrity. We apply the results to real-world web applications, uncovering novel vulnerabilities and verifying the security of fixed versions.