Verifying Code That Calls Code You Can't Trust • Sophia Drossopoulou • Bug Bash EU 2026
Title history
- Verifying Code That Calls Code You Can't Trust • Sophia Drossopoulou • Bug Bash EU 2026 — observed on 20261102-0910 UTC (YouTube)
Keywords
Summary
163 words
Critical Evaluation
Value of the Information & Strength of the Argument
The talk presents a novel formal framework for reasoning about effects of untrusted code, introducing original concepts like ‘protected objects’ and ‘scoped invariants’. The argumentation is rigorous: each definition is precise, proof rules are given, and soundness is discussed. Concrete examples (shop, account, escrow) demonstrate the utility. The treatment of circular specifications via stratification shows deep theoretical insight. However, the presentation is dense and assumes strong background in formal verification, which may limit accessibility. The claims are well-supported by formal proofs and prototype implementations.
Scientific Rigor, Source Quality, Title Accuracy
The scientific rigor is high: the work builds on established Hoare logic and extends it carefully, with soundness proofs (handwritten) and a running prototype in Dafny. The speaker cites collaborators and prior work (ownership types, object capabilities) and mentions historical incidents (Parity Multisig) to motivate the approach. The title precisely matches the content, focusing on verification of code that calls untrusted code. No audience comments are provided, so public reception cannot be assessed.
172 words
Title / Content Match
The title accurately reflects the core topic: verifying code that interacts with untrusted external code, focusing on capabilities, effects, and invariants.
Quality & Reliability
8/10
Keynote address by a distinguished professor (Imperial College, Dahl-Nygaard Prize winner), presenting rigorous formal methods with proofs and tool prototypes. The talk is well-structured, technically deep, and grounded in concrete examples.
Key Moments
Markers derived by PSI from the transcript: the creator did not define chapters.
Cited Sources
- Bug Bash EU 2026 — Conference page where the talk was recorded.
- Sophia Drossopoulou on LinkedIn — Speaker's professional profile.
- GOTO Conferences on Bluesky — Official social media account of the conference.
- GOTO Conferences on LinkedIn — Official LinkedIn page of the conference.
Contribution & Novelties
The talk introduces a novel specification language and inference system for open systems, combining capabilities and scoped invariants to reason about effects of untrusted calls. The approach is distinguished by its ability to specify emergent behavior and handle circular definitions via stratification. The mediation example shows practical risk management. This is original research with formal foundations and a prototype, advancing the state of the art in formal verification of realistic software.
Pour aller plus loin :
- Capability-based security — Related concept for restricting access rights.
- Formal verification — Overview of techniques used in the talk.
- Hoare logic — Basis of the inference system.
- Dafny (programming language) — Tool used for mechanization.
111 words
Radar Profile
The radar shows very high scores in technical level and fiabilité, with slightly lower but still substantial scores in quantity and quality of information. This profile reflects a deep, highly specialized formal-methods talk aimed at experts, with strong methodological foundations.