Modern distributed systems often rely on databases that achieve scalability by providing only weak guarantees about the consistency of data - i.e. weak consistency levels. In these databases executions may happen which are not serialisable, and one problem is thus to understand whether a given transactional application performs only serialisable executions. In this talk first we formally define Parallel Snapshot Isolation (PSI), a consistency level fit for geo-replicated databases, that appeared recently in the literature. The formal definition let us sketch a robustness criterion for PSI, that is a condition to check whether a transactional application generates only serialisable executions, even if ran over a database implementing PSI. We also show how to strengthen PSI by using entity groups, and we sketch a robustness criterion for this consistency level.

The security of cryptographic libraries relies on both the security of the underlying cryptographic primitives and their correct implementation. To obtain strong security guarantees, it is desirable to develop formal computer-checked proofs for both since it is difficult to deal with the inherent complexity and to prevent mismatches between algorithmic specifications and implementations otherwise. In this talk, I will focus on computer-aided proofs of key exchange protocols and pairing-based crypto. In particular, I will present a new modular security proof for key exchange protocols in EasyCrypt and a new tool that supports extremely compact, and often fully automated, proofs of cryptographic constructions based on pairing groups. The tool uses a new formal logic which captures key reasoning principles in provable security, and operates at a level of abstraction that closely matches cryptographic practice. To obtain stronger guarantees and allow for proof reuse in different contexts, the tool also generates proofs that are independently verifiable in EasyCrypt.

In this dissertation we investigate two fundamental aspects of cybercrime: the infection of machines used to monetize the crime and the malicious server infrastructures that are used to manage the infected machines. In the first part of this dissertation, we analyze how fast software vendors apply patches to secure client applications, identifying shared code as an important factor in patch deployment. Shared code is code present in multiple programs. When a vulnerability affects shared code the usual linear vulnerability life cycle is not anymore effective to describe how the patch deployment takes place. In this work we show which are the consequences of shared code vulnerabilities and we demonstrate two novel attacks that can be used to exploit this condition. In the second part of this dissertation we analyze malicious server infrastructures, our contributions are: a technique to cluster exploit server operations, a tool named CyberProbe to perform large scale detection of different malicious servers categories, and RevProbe a tool that detects silent reverse proxies. We start by identifying exploit server operations, that are, exploit servers managed by the same people. We investigate a total of 500 exploit servers over a period of more 13 months. We have collected malware from these servers and all the metadata related to the communication with the servers. Thanks to this metadata we have extracted different features to group together servers managed by the same entity (i.e., exploit server operation), we have discovered that 2/3 of the operations have a single server while 1/3 have multiple servers. Next, we present CyberProbe a tool that detects different malicious server types through a novel technique called adversarial fingerprint generation (AFG). The idea behind CyberProbe's AFG is to run some piece of malware and observe its network communication towards malicious servers. Then it replays this communication to the malicious server and outputs a fingerprint (i.e. a port selection function, a probe generation function and a signature generation function). Once the fingerprint is generated CyberProbe scans the Internet with the fingerprint and finds all the servers of a given family. We have performed a total of 11 Internet wide scans finding 151 new servers starting with 15 seed servers. This gives to CyberProbe a 10 times amplification factor. Moreover we have compared CyberProbe with existing blacklists on the internet finding that only 40% of the server detected by CyberProbe were listed. To enhance the capabilities of CyberProbe we have developed RevProbe, a reverse proxy detection tool that can be integrated with CyberProbe to allow precise detection of silent reverse proxies used to hide malicious servers. RevProbe leverages leakage based detection techniques to detect if a malicious server is hidden behind a silent reverse proxy and the infrastructure of servers behind it. At the core of RevProbe is the analysis of differences in the traffic by interacting with a remote server.

To boost performance, modern transactional systems provide weaker consistency guarantees than those defined by serialisability. Such transactional systems exhibit subtle behaviours that make it difficult for programmers to write correct applications. This problem is complicated by the fact that consistency models specifications are often informal, or they use disparate formalisms.

I will present a framework for specifying transactional consistency model. Then I will focus on Snapshot Isolation, a well-known consistency model, and show how a thorough analysis of its formal specification leads to deriving a static analysis technique for performing transaction chopping under Snapshot Isolation.

I'll report on a case study in secure programming, focusing on the design, implementation and auditing of programs for playing the board game Battleship. I'll begin by precisely defining the security of Battleship programs, borrowing the real/ideal paradigm of theoretical cryptography. I'll then consider three implementations of Battleship: one in Concurrent ML featuring a trusted referee; one in Haskell/LIO using information flow control to avoid needing a trusted referee; and one in Concurrent ML using access control to avoid needing such a referee. All three implementations employ data abstraction in key ways.