Jacob Ginesin

I'm an undergraduate at Northeastern University double-majoring in computer science and mathematics. I'm interested in the formalization and verification of interesting and useful systems, as well as the logical foundations of mathematics and computing. My previous work involves system and network security. I'm thankful to have worked under the various supervisions of Cristina Nita-Rotaru and Gunar Schirner at Northeastern University, Jelena Mirkovic at USC, and Christoph Haase at Oxford.


Contact Me

Please reach out by email: ginesin (dot) j (at) northeastern (dot) edu
Alternatively, I'm on other platforms: LinkedIn, and GitHub.

Publications

* indicates equal contribution.

A Formal Analysis of SCTP: Attack Synthesis and Patch Verification

Jacob Ginesin*, Max von Hippel*, Evan Defloor, Cristina Nita-Rotaru, Michael Tüxen. USENIX Security 2024.

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.

The State of Julia for Scientific Machine Learning

Edward Berman*, Jacob Ginesin*. To appear at the NeurIPS Machine Learning and Physical Sciences Workshop (Oral Spotlight)

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

Can It Edit? Evaluating the Ability of Large Language Models to Follow Code Editing Instructions

Federico Cassano, Luisa Li, Akul Sethi, Noah Shinn, Abby Brennan-Jones, Jacob Ginesin, Edward Berman, George Chakhnashvili, Anton Lozhkov, Carolyn Jane Anderson, Arjun Guha. Conference on Language Modeling, 2024.

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

Understanding DNS Query Composition at B-Root

Jacob Ginesin, Jelena Mirkovic. IEEE/ACM Conference on Big Data Computing, Applications and Technologies.

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

Preprints

Korg: An Attack Synthesis Tool for Distributed Protocols

Jacob Ginesin, Max von Hippel, Cristina Nita-Rotaru. In submission.

Automatically synthesizing attackers that can replay, reorder, drop, or insert messages onto a channel

ConnILP: Allocating Distributed Communication Design in Domain Platforms for Streaming Applications

Qucheng Jiang, Gunar Schirner, Oscar Kellner, Tianrui Ma, and Jacob Ginesin. In submission.

Optimizing domain-specific hardware configurations via a reduction to integer linear programming!

Other Stuff

Regular Language Bounds: Extraction and Applications (Poster)

Jacob Ginesin, Christoph Haase. Presented at the Joint Mathematical Meetings 2024.

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

The Matrix Reloaded: A Mechanized Formal Analysis of the Matrix Cryptographic Suite

Jacob Ginesin, Cristina Nita-Rotaru. arXiv preprint arXiv:2408.12743, 2024.

We analyze the cryptographic group instant messaging protocols behind Matrix using ProVerif, comparing them to the standard in the space (WhatsApp, Signal, etc.). We find a few issues.

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.

Effective Preconditioning for LOBPCG

Jacob Ginesin, Daniel Yu. Product of a 2024 summer undergraduate research program ran by Northeastern University.

When finding the algebraic connectivity of a graph using the Fiedler value, the 2nd smallest eigenvalue of the graph Laplacian, exploiting said graphical structure to precondition the eigensolver (LOBPCG) is somewhat effective.

Insights from CVE-2021-3772, Clarifying SCTP Specification Flaws

Jacob Ginesin. Extended details of an RFC9260 errata.

We demystify a critical ambiguity in the SCTP spec, RFC9260, which if misinterpreted leads to an off-path attack.

A Simple Heuristic for Deciding Intersection Non-Emptiness for Regular and ω-Regular Automata

Jacob Ginesin. Product of research done while visiting at Oxford.

We define and implement a simple heuristic for deciding the intersection non-emptiness problem for regular and ω-regular automata