Automatic Patch-based Exploit Generation (completed)

When a vulnerability is found, it generally goes through a responsible disclosure process. This means that the vendor will be contacted to write a fix before the vulnerability is made public. The patch will be pushed to its users and the vulnerability details become public. In theory, this is a safe process for vulnerability exposure … full description “Automatic Patch-based Exploit Generation (completed)”

Control-flow graphs for Automatic-Exploit Generation (completed)

Research has shifted over the years when it comes to binary exploitation. With more accurate and practical implementations of Control-flow Integrity (CFI) [1][2], the question arises as to what attack surface is still available – and how to exploit it. In particular, what attacks can be performed when staying within the boundaries of a (perfect) … full description “Control-flow graphs for Automatic-Exploit Generation (completed)”

Formal Verification for Blockchains (available)

In this project you will explore the world of formal verification andblockchains, specifically the new Ethereum 2.0 ‘Proof-of-Stake’ blockchain [1]. This is a more energy-efficient replacement for the original Ethereum ‘Proof-of-Work’ blockchain. As in any blockchain, correctness of thedistributed ‘consensus’ protocol [2] used to maintain the chain and extend it with new blocks is critical. … full description “Formal Verification for Blockchains (available)”

Invisible Malware using Intel SGX Enclaves (completed)

A fundamental security problem when hosting applications on cloud platforms is the increased risk of sensitive data loss (e.g. due to negligent or malicious employees of the cloud provider). An exciting approach to mitigating such attacks are new trusted execution environments (e.g. Intel SGX), recently available on commodity CPUs. Intel SGX allows users to create … full description “Invisible Malware using Intel SGX Enclaves (completed)”