5 papers
From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware
Valentin Bergeron, Karolina Gorna
Enforcing invariants in safety-critical systems is increasingly urgent as AI-generated code becomes widespread. Unfortunately, the runtimes required to support high-level specifica…
From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries
Karolina Gorna, Nicolas Iooss, Yannick Seurin +2
Zorya is a concolic execution framework that lifts compiled binaries to Ghidra's P-Code intermediate representation and uses the Z3 SMT solver to detect vulnerabilities by reasonin…
Zorya: Automated Concolic Execution of Single-Threaded Go Binaries
Karolina Gorna, Nicolas Iooss, Yannick Seurin +1
Go's adoption in critical infrastructure intensifies the need for systematic vulnerability detection, yet existing symbolic execution tools struggle with Go binaries due to runtime…
Exposing Go's Hidden Bugs: A Novel Concolic Framework
Karolina Gorna, Nicolas Iooss, Yannick Seurin +1
The widespread adoption of the Go programming language in infrastructure backends and blockchain projects has heightened the need for improved security measures. Established techni…
Self-Sovereign Identity for Consented and Content-Based Access to Medical Records using Blockchain
Marie Tcholakian, Karolina Gorna, Maryline Laurent +2
Electronic Health Records (EHRs) and Medical Data are classified as personal data in every privacy law, meaning that any related service that includes processing such data must com…