Showing 1–6 of 6 results for author: Ginesin, J

The State of Julia for Scientific Machine Learning

Authors: Edward Berman, Jacob Ginesin

Abstract: Julia has been heralded as a potential successor to Python for scientific machine learning and numerical computing, boasting ergonomic and performance improvements. Since Julia's inception in 2012 and declaration of language goals in 2017, its ecosystem and language-level features have grown tremendously. In this paper, we take a modern look at Julia's features and ecosystem, assess the current st… ▽ More Julia has been heralded as a potential successor to Python for scientific machine learning and numerical computing, boasting ergonomic and performance improvements. Since Julia's inception in 2012 and declaration of language goals in 2017, its ecosystem and language-level features have grown tremendously. In this paper, we take a modern look at Julia's features and ecosystem, assess the current state of the language, and discuss its viability and pitfalls as a replacement for Python as the de-facto scientific machine learning language. We call for the community to address Julia's language-level issues that are preventing further adoption. △ Less

Submitted 20 December, 2024; v1 submitted 13 October, 2024; originally announced October 2024.

Comments: Presented at the 2024 NeurIPS Machine Learning and the Physical Sciences Workshop

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

Authors: Jacob Ginesin, Cristina Nita-Rotaru

Abstract: Secure instant group messaging applications such as WhatsApp, Facebook Messenger, Matrix, and the Signal Application have become ubiquitous in today's internet, cumulatively serving billions of users. Unlike WhatsApp, for example, Matrix can be deployed in a federated manner, allowing users to choose which server manages their chats. To account for this difference in architecture, Matrix employs t… ▽ More Secure instant group messaging applications such as WhatsApp, Facebook Messenger, Matrix, and the Signal Application have become ubiquitous in today's internet, cumulatively serving billions of users. Unlike WhatsApp, for example, Matrix can be deployed in a federated manner, allowing users to choose which server manages their chats. To account for this difference in architecture, Matrix employs two novel cryptographic protocols: Olm, which secures pairwise communications, and Megolm, which relies on Olm and secures group communications. Olm and Megolm are similar to and share security goals with Signal and Sender Keys, which are widely deployed in practice to secure group communications. While Olm, Megolm, and Sender Keys have been manually analyzed in the computational model, no symbolic analysis nor mechanized proofs of correctness exist. Using mechanized proofs and computer-aided analysis is important for cryptographic protocols, as hand-written proofs and analysis are error-prone and often carry subtle mistakes. Using Verifpal, we construct formal models of Olm and Megolm, as well as their composition. We prove various properties of interest about Olm and Megolm, including authentication, confidentiality, forward secrecy, and post-compromise security. We also mechanize known limitations, previously discovered attacks, and trivial attacker wins from the specifications and previous literature. Finally, we model Sender Keys and the composition of Signal with Sender Keys in order to draw a comparison with Olm, Megolm, and their composition. From our analysis we conclude the composition of Olm and Megolm has comparable security to the composition of Signal and Sender Keys if Olm pre-keys are signed, and provably worse post-compromise security if Olm pre-keys are not signed. △ Less

Submitted 7 December, 2024; v1 submitted 22 August, 2024; originally announced August 2024.

Comments: 16 pages, 6 figures

ACM Class: C.2.2; E.3

A Formal Analysis of SCTP: Attack Synthesis and Patch Verification

Authors: Jacob Ginesin, Max von Hippel, Evan Defloor, Cristina Nita-Rotaru, Michael Tüxen

Abstract: SCTP is a transport protocol offering features such as multi-homing, multi-streaming, and message-oriented delivery. Its two main implementations were subjected to conformance tests using the PacketDrill tool. Conformance testing is not exhaustive and a recent vulnerability (CVE-2021-3772) showed SCTP is not immune to attacks. Changes addressing the vulnerability were implemented, but the question… ▽ More SCTP is a transport protocol offering features such as multi-homing, multi-streaming, and message-oriented delivery. Its two main implementations were subjected to conformance tests using the PacketDrill tool. Conformance testing is not exhaustive and a recent vulnerability (CVE-2021-3772) showed SCTP is not immune to attacks. Changes addressing the vulnerability were implemented, but the question remains whether other flaws might persist in the protocol design. We study the security of the SCTP design, taking a rigorous approach rooted in formal methods. We create a formal Promela model of SCTP, and define 10 properties capturing the essential protocol functionality based on its RFC specification and consultation with the lead RFC author. Then we show using the Spin model checker that our model satisfies these properties. We define 4 attacker models - Off-Path, where the attacker is an outsider that can spoof the port and IP of a peer; Evil-Server, where the attacker is a malicious peer; Replay, where an attacker can capture and replay, but not modify, packets; and On-Path, where the attacker controls the channel between peers. We modify an attack synthesis tool designed for transport protocols, Korg, to support our SCTP model and four attacker models. We synthesize 14 unique attacks using the attacker models - including the CVE vulnerability in the Off-Path attacker model, 4 attacks in the Evil-Server attacker model, an opportunistic ABORT attack in the Replay attacker model, and eight connection manipulation attacks in the On-Path attacker model. We show that the proposed patch eliminates the vulnerability and does not introduce new ones according to our model and protocol properties. Finally, we identify and analyze an ambiguity in the RFC, which we show can be interpreted insecurely. We propose an erratum and show that it eliminates the ambiguity. △ Less

Submitted 8 March, 2024; originally announced March 2024.

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

Authors: Federico Cassano, Luisa Li, Akul Sethi, Noah Shinn, Abby Brennan-Jones, Jacob Ginesin, Edward Berman, George Chakhnashvili, Anton Lozhkov, Carolyn Jane Anderson, Arjun Guha

Abstract: A significant amount of research is focused on developing and evaluating large language models for a variety of code synthesis tasks. These include synthesizing code from natural language, synthesizing tests from code, and synthesizing explanations of code. In contrast, the behavior of instructional code editing with LLMs is understudied. These are tasks in which the model is provided a block of c… ▽ More A significant amount of research is focused on developing and evaluating large language models for a variety of code synthesis tasks. These include synthesizing code from natural language, synthesizing tests from code, and synthesizing explanations of code. In contrast, the behavior of instructional code editing with LLMs is understudied. These are tasks in which the model is provided a block of code and an instruction to modify the code. The editing instruction may ask for a feature to be added or removed, describe a bug and ask for a fix, or ask for a different kind of solution. We introduce a carefully crafted benchmark of code editing tasks and use it to evaluate several cutting edge LLMs. Our evaluation exposes a significant gap between the capabilities of state-of-the-art open and closed models. For example, even GPT-3.5-Turbo is better than the best open model at code editing tasks. We also introduce a new, carefully curated, permissively licensed training dataset of code editing tasks coupled with natural language instructions. Using this training dataset, we show that we can fine-tune open Code LLMs to significantly improve their code editing capabilities, closing the gap between open and closed models. All code, data, and models are available at https://github.com/nuprl/CanItEdit. △ Less

Submitted 23 September, 2024; v1 submitted 10 December, 2023; originally announced December 2023.

Understanding DNS Query Composition at B-Root

Authors: Jacob Ginesin, Jelena Mirkovic

Abstract: The Domain Name System (DNS) is part of critical internet infrastructure, as DNS is invoked whenever a remote server is accessed (an URL is visited, an API request is made, etc.) by any application. DNS queries are served in hierarchical manner, with most queries served locally from cached data, and a small fraction propagating to the top of the hierarchy - DNS root name servers. Our research aims… ▽ More The Domain Name System (DNS) is part of critical internet infrastructure, as DNS is invoked whenever a remote server is accessed (an URL is visited, an API request is made, etc.) by any application. DNS queries are served in hierarchical manner, with most queries served locally from cached data, and a small fraction propagating to the top of the hierarchy - DNS root name servers. Our research aims to provide a comprehensive, longitudinal characterization of DNS queries received at B-Root over ten years. We sampled and analyzed a 28-billion-query large dataset from the ten annual Day in the Life of the Internet (DITL) experiments from 2013 through 2022. We sought to identify and quantify unexpected DNS queries, establish longitudinal trends, and compare our findings with published results of others. We found that unexpected query traffic increased from 39.57% in 2013 to 67.91% in 2022, with 36.55% of queries being priming queries. We also observed growth and decline of Chromium-initiated, random DNS queries. Finally, we analyzed the largest DNS query senders and established that most of their traffic consists of unexpected queries. △ Less

Submitted 15 August, 2023; originally announced August 2023.

Comments: 20 pages with 18 figures and 1 table. Published and presented at the 2022 IEEE/ACM International Conference on Big Data Computing, Applications and Technologies (BDCAT)

ACM Class: C.2.2

SafeLLVM: LLVM Without The ROP Gadgets!

Authors: Federico Cassano, Charles Bershatsky, Jacob Ginesin, Sasha Bashenko

Abstract: Memory safety is a cornerstone of secure and robust software systems, as it prevents a wide range of vulnerabilities and exploitation techniques. Among these, we focus on Return-Oriented Programming (ROP). ROP works as such: the attacker takes control of the program's execution flow via a memory corruption attack, then takes advantages of code snippets already in the program's memory, dubbed "gadg… ▽ More Memory safety is a cornerstone of secure and robust software systems, as it prevents a wide range of vulnerabilities and exploitation techniques. Among these, we focus on Return-Oriented Programming (ROP). ROP works as such: the attacker takes control of the program's execution flow via a memory corruption attack, then takes advantages of code snippets already in the program's memory, dubbed "gadgets," to achieve the attacker's desired effect. In this paper, we introduce SafeLLVM, an approach to minimize the number of gadgets in x86-64 binaries compiled with the LLVM infrastructure. Building upon the techniques outlined in previous works, we implement a series of passes within the LLVM compiler's backend to minimize the number of gadgets present and thus prevent ROP attacks. We evaluated our approach by compiling a number of real-world applications, including cJSON, zlib, curl, and mimalloc. The results show our solution is able to prevent any form of ROP on the binaries compiled with SafeLLVM while maintaining the same functionality as the original binaries. △ Less

Submitted 1 November, 2023; v1 submitted 10 May, 2023; originally announced May 2023.