Disciplined techniques for the analysis and protection of security-critical systems

In the last years most of our daily activities have moved to the digital world, including sensitive operations related to health data management and financial processes. Security flaws in the systems running these critical operations may have a serious impact on our society, ranging from breaches of citizens privacy to severe economical damages. Several aspects must be taken into account when reasoning on the security of critical systems, comprising the security of the networks where they are hosted and the security of web applications running on these systems. Additional threats are posed by the improper use of cryptography that may allow unintended disclosure of confidential data. In this thesis we propose a set of disciplined techniques for the analysis and protection of security-critical systems regarding these important aspects. For what concerns network security, we propose a technique to decompile firewall policies into abstract specifications giving a high-level description of the firewall behavior. Additionally, we study the problem of cross-compiling policies to different firewall systems. About web security, we survey the techniques proposed in the literature and by web standards to tackle the most common attacks against web sessions and we carefully evaluate them in terms of usability, compatibility with existing websites and ease of deployment. Furthermore, we propose a client-side approach to strengthen the security of Web protocols by monitoring their execution inside the browser. Regarding cryptography, we provide a detailed analysis of Java keystores, encrypted files that are used to securely store cryptographic keys by Java applications. We report novel attacks and weaknesses found in the most widespread keystore implementations and report on the fixes implemented by Java developers after our responsible disclosure.