Title: Static and dynamic enforcement of security via relational reasoning
Language: English
Authors: Grimm, Niklas 
Qualification level: Doctoral
Advisor: Maffei, Matteo 
Issue Date: 2021
Number of Pages: 321
Qualification level: Doctoral
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.
Keywords: Web Security; Cryptographic Protocols; Information Flow Control; Noninterference; Language Based Security; Type Systems
URI: https://doi.org/10.34726/hss.2021.90710
DOI: 10.34726/hss.2021.90710
Library ID: AC16206749
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on Jun 20, 2021


checked on Jun 20, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.