Blockchain smart contracts have created a rapidly-expanding environment with a new programming model and high demand for security-critical applications. We aim to use information flow techniques to analyze and secure a range of smart contract applications.
Server Side Template Injection (SSTI) is a recent type of vulnerability that exploits the fact that adversarial inputs are inserted into templates that are rendered by a so called template engine. To the best of our knowledge only 2 solutions have been developed to detect and exploit SSTI, Burp Suite and Tplmap. These solutions are either proprietary software (Burp Suite), or have a limited amount of (fixed) payloads that are restricted to a limited number of template engines (Tplmap). This latter approach not only reduces the scope of the tool to specific template engines, but also can be easily defeated by simple black-listing of such payloads. In this work, we introduce a solution that automatically detects and exploits Server Side Template Injection (SSTI) vulnerabilities making use of techniques that generalize the previous tool to a broader number of template engines, and that dynamically generates the exploit payloads using an exploit generation grammar specific for each language. This solution is being integrated as plug-in for a widely used open-source penetration testing tool to find web application vulnerabilities.
The cryptocurrency Ethereum offers a Turing-complete language for programming distributed programs that are executed on the Ethereum blockchain and control the flow of the digital currency Ether - so called smart contracts. Flawed smart contracts impose a big financial risk and therefore call for static analysis, but it turns out that analysing Ethereum smart contracts is particularly challenging due to the expressiveness of the underlying language and because of the peculiarities of the distributed, asynchronous execution environment. In this talk I will briefly introduce Ethertrust, the first sound static analysis for Ethereum smart contracts, which outperforms the state-of-the-art in precision and efficiency. The foundations of our analysis and the tool will be presented in detail in a CAV tutorial on July 13th.
In this talk, I will present WPSE, a browser-side security monitor for web protocols designed to ensure compliance with the intended protocol flow, as well as confidentiality and integrity properties of messages. WPSE is expressive enough to protect web applications from a wide range of protocol implementation bugs and web attacks (e.g., XSS). I will discuss concrete examples of attacks which can be prevented by WPSE on OAuth 2.0 and SAML 2.0, including a new attack on the Google implementation of SAML 2.0 which we discovered by formalizing the protocol specification in WPSE. This work will be presented at Usenix Security ’18.
Quantitative information flow usually assumes that we are able to compute the channel matrix of the system. This is the so-called white-box assumption. Often, however, the system is not entirely known, or it is too complicated to be able to extract the conditional probabilities that relate inputs and observables. The extreme case in which we don't assume any knowledge of the system's internal mechanisms is called black-box assumption. To the best of our knowledge, the only method proposed so far to estimate the leakage under the black-box assumption relies on a frequentist approach (the authors developed also tool called LeakWatch). We propose a new method based on Machine Learning, and we compare it with the frequentist one, showing favorable results in terms of efficiency.
WireGuard is a newly proposed secure virtual private network (VPN) tunnel that will soon be integrated into the Linux kernel. We prove all secrecy and authentication properties WireGuard claims to have (i.e. forward secrecy, mutual authentication resistant against key compromise impersonation attacks, resistance against unknown key-share attacks, and resistance against replays), and we work on proving identity hiding and resistance against distributed denial of service. The proof is done using the CryptoVerif cryptographic protocol verifier which works in the computational model and produces proofs as sequences of games. This is joint work with Bruno Blanchet, Karthikeyan Bhargavan, and Harry Halpin.
BitML is a process calculus for smart contracts which can be compiled to sets of standard Bitcoin transactions. Our BitML compiler enjoys computational soundness: any computational (Bitcoin-level) attack against a compiled contract has a correspondent symbolic (BitML-level) attack.
Probabilistic hyperproperties can express useful policies such as probabilistic noninterference, quantitative information flow, and differential privacy as well as other interesting requirements such as probabilistic causation. In this talk, I will briefly discuss our work on temporal logics for expressing probabilistic hyperproperties and the related model checking algorithms.
Despite the conceptual simplicity of distance-bounding (DB) protocols, devising a formal characterization of DB protocols that is amenable to automated formal analysis is non-trivial, primarily because of their real-time and probabilistic nature. We propose a rewriting logic framework for formal analysis of different forms of distance-fraud attacks, and use it to (mechanically) verify false-acceptance and false-rejection probabilities under various settings and attacker models.
We present a scalable and efficient optimization techniques to find the optimal defence strategy over probabilistic attack trees. The technique is based on integer linear programming, is based on unimodular matrices and can find the optimal solution over trees with 2^(500) paths in under 3 minutes
Abstract: Energy harvesting enables novel devices and applications without batteries. However, intermittent operation under energy harvesting poses new challenges to preserving program semantics under power failures. I will talk about our ongoing work on developing a static analysis tool for automatically identifying bugs caused by I/O operations and methods for fixing such bugs.