$ whoami

Hi, welcome!

I am Karolina, a Ph.D. candidate in cybersecurity at Télécom Paris and Ledger Donjon. My research combines formal verification methods with practical security engineering to address vulnerabilities in production systems.

// warning: rabbit holes ahead

Research Interests

▹Symbolic execution and formal verification of protocols,
▹Software and networks security,
▹Binaries analysis,
▹Secure compilation and hardware-software interactions,
▹Zero-knowledge proof systems,
▹Languages: Rust, Go, Assembly.

When things are beautifully done, there is usually a well thought out sort of abstraction layers.

Jim Keller

// it works on my machine

My Current Main Project

active

I'm the main developer of ZORYA, a concolic execution framework for binary-level vulnerability analysis, with a strong focus on Go binaries. Written in Rust, it initializes execution from real runtime state (CPU + memory dumps), translates code to Ghidra's low-level P-Code, and explores paths with concrete and symbolic values using the Z3 SMT solver.

View on GitHub

karolina@donjon:~/zorya

$ zorya tests/programs/crashme-go/crashme-go \

--lang go --compiler tinygo --mode main

[zorya] init state from CPU + memory dump

[zorya] lifting to Ghidra P-Code

[zorya] solving paths (concrete + symbolic) via Z3

[found] nil pointer dereference @ crashme.crash

[done] results written to results/

// ship first, sleep later

Innovation & Prototyping

Applied research requires iteration between theoretical frameworks and empirical validation. Through competitive hackathons and collaborative prototyping events, I develop proof-of-concept implementations that test security hypotheses in constrained timeframes. This rapid experimentation informs my doctoral research by exposing practical limitations of formal methods, revealing emergent attack vectors in Layer 2 systems, and fostering interdisciplinary collaboration. The projects below demonstrate how theoretical security analysis translates into functional tools and protocols.