SERICS Summer School on Secure Software Development

Prof. Matteo Maffei delivered a lecture “Foundations of Secure Blockchain Programming”, exploring the key principles, challenges, and best practices of writing secure blockchain software. He outlined major threats — including smart contract vulnerabilities, reentrancy attacks, front-running, and flawed consensus logic — and stressed that despite blockchain’s immutability and transparency, implementations remain prone to costly errors. He discussed secure coding practices such as formal verification, runtime checks, gas-cost awareness, and language choice, and compared programming frameworks in terms of safety and usability. He also highlighted essential tools like automated testing, fuzzing, static analysis, and code audits, as well as advanced techniques such as symbolic execution and model checking.

Through case studies of real incidents, Prof. Maffei showed how vulnerabilities could have been prevented by applying these principles. The lecture, attended by students, researchers, and practitioners, concluded with a lively discussion on scalability, privacy, and regulatory aspects. Prof. Maffei emphasized that combining theory — formal methods and secure design — with practice — auditing, testing, and tooling — is crucial for building robust blockchain applications.

Markus Scherer introduced Wanilla, a new tool designed to make WebAssembly (Wasm) programs more secure. Wasm is a modern technology used to run software across many platforms and is increasingly important in areas where security matters, such as web services and smart contracts. While Wasm was carefully designed, programs written in it can still have vulnerabilities, especially when translated from older, less secure programming languages. Wanilla helps address this by automatically checking whether information inside a program stays protected and whether different parts of the program interact safely. Built on the HoRSt analysis framework, Wanilla uses advanced methods to detect potential leaks or memory errors before the program runs. In tests with both synthetic examples and real-world smart contracts, Wanilla showed strong performance, often more effective than existing tools. Scherer’s talk highlighted how this innovation strengthens the reliability of WebAssembly and supports its safe use in critical applications.

Pedro Bernardo, in his talk, addressed how browsers implement client-side security features such as cookie settings and “mixed content” rules that prevent secure pages from loading insecure resources. These mechanisms are designed to keep users safe, but they are complex, and both their design and implementation can contain bugs. He presented a framework that leverages Web Platform Tests (WPT) — a large suite of tests across different browsers—to monitor actual browser behavior, collect “execution traces” (records of what happens internally), and verify them against formal rules called Web invariants, security properties that should always hold. Using this framework, the team tested nine security invariants and discovered violations in 104 WPT tests across Firefox, Chromium, and Safari. These violations have concrete security implications. The researchers reported their findings to browser vendors and standards bodies, and one issue was assigned a CVE in Safari.

The presentation demonstrated that automated, formal checking of browser behavior can uncover security flaws that might otherwise go unnoticed, ultimately contributing to a safer Web for all users.