CySec members contribute to CSF 2024
The Computer Security Foundations Symposium (CSF) is an annual conference for researchers to explore security theories, formal models, and verification techniques in computer security. Key topics include access control, information flow, cryptographic protocols, database security, language-based security, authorization, trust, verification, integrity, availability, and the role of formal methods in security research. At the 37th IEEE Computer Security Foundations Symposium (CSF 2024), held in Enschede, The Netherlands, from July 8-12, two research teams from CySec presented their findings on the intersection of theoretical computer science and computer security.
Markus Scherer presented an innovative approach developed as part of the CDL-BOT project, titled “Wappler: Sound Reachability Analysis for WebAssembly,” co-authored with Jeppe Fredsgaard Blaabjerg, Alexander Sjösten, Magdalena Solitro, and Matteo Maffei. The presentation focused on enhancing the security and performance of WebAssembly (Wasm), a low-level language increasingly used in critical areas like web browsers, smart contracts, and edge computing.
Given the critical need to identify and eliminate bugs and security vulnerabilities in these domains, Scherer introduced Wappler, the first fully sound and automated static analysis technique for WebAssembly. The team tackled several challenges due to the inherent complexity of Wasm’s formal semantics, its embedding in potentially malicious contexts, and its low-level nature, which complicates memory management and other core features. The Wappler approach works by encoding Wasm semantics into Horn clauses, making it accessible to automated theorem provers like z3. This innovative technique required addressing Wasm’s unsuitability for automated security proofs by introducing annotations for a precise and sound encoding. Scherer and his team also developed a formalism to specify embedder behavior and created a sound yet precise memory abstraction to handle the complexities of Wasm environments.
The team demonstrated the flexibility of their logical formalism by encoding various general and Wasm-specific security properties. Additionally, their experimental evaluation on the official Wasm test suite showcased Wappler’s performance and effectiveness, making it a significant contribution to the field of WebAssembly security.
Stefano Trevisani presented the paper On Efficient and Secure Compression Functions for Arithmetization-Oriented Hashing. In collaboration with Elena Andreeva, Rishiraj Bhattacharyya, and Arnab Roy, he introduced PGV-LC compression modes to construct efficient and secure algebraic hash functions for Verifiable Computation, privacy-preserving Blockchains, and Zero-Knowledge SNARKs/STARKs. The researchers presented advancements in ZK-SNARKs, crucial for privacy-oriented payment systems, identity protocols, and anonymous voting systems, with a focus on improving the efficiency of Merkle Tree (MT) opening proofs, commonly verified through SNARK systems.
Traditional hash functions like SHA-2 are inefficient in SNARK frameworks, leading the team to explore Arithmetization-Oriented (AO) cryptographic designs as a promising alternative. They introduced two new AO blockcipher-based compression modes, PGV-LC and PGV-ELC, extending the classical PGV approach. The Poseidon-DM hash function, instantiated by using PGV-LC, offers up to a 3x speed-up for native X86 execution and a 50% speed-up in the Groth16 SNARK framework compared to Poseidon. The work also demonstrates how wide arities can drastically improve the efficiency of Merkle Tree (MT) accumulators: An optimal choice of the arity allows Poseidon-DM to be up to 9x faster natively and up to 2.5x faster in Groth16, compared to Poseidon over binary trees.