WebAssembly is a new low-level programming language designed with the goal to increase interoperability and security across the software ecosystem. The WebAssembly specification is defined by the World Wide Web Consortium, with a multitude of implementors, ranging from browsers to standalone runtimes.
In order to ensure adherence to the specification, some WebAssembly implementations use formally-verified interpreters as testing oracles. This thesis explores a novel approach to designing a formally-verified interpreter, by using an intrinsically-typed representation of the WebAssembly syntax.
This intrinsically-typed interpreter is implemented in the Lean 4 proof assistant, leveraging its functional-but-in-place features to achieve good performance without sacrificing functional purity.
The transformative potential of deep learning in enhancing computer science solutions has not gone unnoticed in the fields of security and privacy. However, the sheer volume of related scientific literature and the significant gap between a lab context and real-world environments make it extremely challenging to assess the current progress in the area. In this talk, I will review underlying mechanisms and main principles behind deep learning when applied to offensive and defensive cybersecurity solutions. I will focus on two primary use cases: traffic analysis attacks on Tor and network-based intrusion detection systems, analyzing the expected benefits and potential pitfalls of using deep learning. This analysis effectively challenges the common perception of a purely end-to-end approach. To that end, the presentation emphasizes the importance of explainability and error analysis for validating and troubleshooting deep neural networks. This discussion is meant to equip cybersecurity researchers and practitioners to begin incorporating deep learning in their toolbox while maintaining a critical and holistic perspective.