I'm interested in the formalization and verification of interesting and useful systems, as well as the logical foundations of mathematics and computing. I try to employ hardcore mathematical techniques to solve real-world problems in systems and security.

Representative Publications

A Formal Analysis of SCTP: Attack Synthesis and Patch Verification. USENIX Security 2024, IRTF Applied Networking Research Prize Winner! Jacob Ginesin, Max von Hippel, Evan Defloor, Cristina Nita-Rotaru, Michael Tüxen.

We use formal methods to analyze the security of the Stream Control Transmission Protocol (SCTP). We report a symphony of new attacks across various attacker models, the automated re-discovery of CVE-2021-3772, and two ambiguities in SCTP RFC that, if misinterpreted, enable attacks. [more details]

On Uncertainty Calibration for Equivariant Functions. Transactions on Machine Learning Research 2025. Edward Berman, Jacob Ginesin, Marco Pacini, Robin Walters.

We develop a general theory of uncertainty estimation on functions constrainted to be equivariant with respect to an arbitrary group. We prove some bounds on uncertainty, and show our bounds manifest in practice with a few real-world experiments. [more details]

The State of Julia for Scientific Machine Learning. NeurIPS ML4PS 2024 (Oral Spotlight). Edward Berman, Jacob Ginesin.

How does Julia compare to Python for scientific machine learning tasks? And, is Julia ready for primetime?

Understanding DNS Query Composition at B-Root. IEEE/ACM Conference on Big Data Computing, Applications and Technologies 2023. Jacob Ginesin, Jelena Mirkovic.

We study the validity of traffic at a DNS root server through analyzing historical data. [more details]

More Stuff

SAGA: A Security Architecture for Governing AI Agentic Systems. Network and Distributed System Security (NDSS) Symposium 2025. Georgios Syros, Anshuman Suri, Jacob Ginesin, Cristina Nita-Rotaru, Alina Oprea.

A distributed authentication scheme in a similar flavor to distributed Kerberos, but with some modifications to better suit AI agents. I wrote several cryptographic models to formally verify our protocol design maintains secrecy and authentication, available here!

Regular Language Bounds: Extraction and Applications (Poster). Joint Mathematical Meetings 2024. Jacob Ginesin, Christoph Haase.

We define methods to compute the upper and lower boundaries of regular languages in order to speed up model checkers.

Can It Edit? Evaluating the Ability of Large Language Models to Follow Code Editing Instructions. COLM 2024. Federico Cassano, Luisa Li, Akul Sethi, Noah Shinn, Abby Brennan-Jones, Jacob Ginesin, Edward Berman, George Chakhnashvili, Anton Lozhkov, Carolyn Jane Anderson, Arjun Guha.

We develop benchmarks to evaluate large language models on code editing performance, as previous benchmarks were insufficient. We also fine-tune models for specifically code editing.

SafeLLVM: LLVM Without The ROP Gadgets!. Federico Cassano, Charles Bershatsky, Jacob Ginesin, Sasha Bashenko. arXiv preprint arXiv:2305.06092, 2023.

A Return-oriented programming attack is when an attacker takes advantage of existing chunks of code in memory, dubbed gadgets, and chains them together to form an attack. We propose an approach to minimize the number of usable gadgets in compiled binaries, extending the methodology of a previous work.

Even More Stuff

Since you've scrolled so far, I suppose you might be interested in my other output...

• My GRFP research proposal on provable security for implementations of the Signal Protocol. Inspired by a conversation with Wolfe Schmidt at USENIX Security.
• Ahead-of-Time Detection of Instruction Cache Timing Attacks With Towers of Interpreters. My hardware security final project, an extension of Amin and Chlipala's paper.
• On Establishing Cryptocurrencies as Securities and Replication: Security Analysis of Ripple Consensus - thoroughly proving XRP/Ripple is a complete scam.
• Provable Performance Guarantees for Byzantine Systems. Some semi-complete work on the parametric timed I/O Buchi Automata.
• Effective Preconditioning for LOBPCG. Product of a summer undergraduate mathematics research program ran by Northeastern University. Exploiting graphical structure in matrices to improve iterative numerical techniques.
• Insights from CVE-2021-3772, Clarifying SCTP Specification Flaws. Extended details of this RFC9260 errata.
• A Simple Heuristic for Deciding Intersection Non-Emptiness for Regular and ω-Regular Automata. Product of some research done while visiting at Oxford.
• Sender Keys. A wikipedia article I wrote on the secure group communication protocol used by Signal, WhatsApp, and FB Messenger.
• Cure53 Audit Report: Obscura Protocol. A sample security audit I contributed to for the Obscura VPN, which tunnels application traffic through QUIC using the IETF's MASQUE protocol. I was responsible for vulnerabilities 003, 004, 005, and 006.

Since you've read this far, I'm seeking collaborators interested in working on highly practical formally verified software, especially for high-stakes cryptographic and security-intensive systems. If this is you, hit my line.