Cybersecurity Commons^™

2026 Cyber-Resilient Health Care Workshop Report, Malcolm Schongalla, Sergey Bratus

Computer Science Technical Reports

The ISTS and the Dartmouth College Cybersecurity Cluster hosted the successful, inaugural Cyber-Resilient Health Care (CRHC) Workshop, March 5th & 6th, 2026. The event theme was "Innovation and Implementation," in response to the need to shift from reactive to proactive resiliency measures in the healthcare sector. Approximately 30 experts in clinical health care, cybersecurity, medical technology, policy, and innovation met to discuss solution-focused innovations addressing hard, cyber-related problems in health care. The agenda featured keynotes, an expert panel, innovation pitches, small group discussions, and a tabletop infrastructure disaster exercise. Participants gained insights into the obstacles and solutions involved in supporting …

Weavecc: Symbolically-Guided Joint Exploration Of Inputs And Schedules For Concurrency Bug Detection, William Philip Dinauer

Dartmouth College Master’s Theses

Concurrent programs introduce a class of bugs that depend jointly on both program inputs and thread schedules. Exposing these bugs requires simultaneously reasoning about which code paths are reachable and which thread interleavings are possible. At the same time, many existing tools handle the problem insufficiently. Race detectors observe only the interleavings that the OS happens to produce. Fuzzers explore inputs without controlling schedules. Tools that address both dimensions together exist, but are built on interpretation-based symbolic executors that incur considerable overhead.

We present WeaveCC, a practical concurrency testing tool for C/C++ programs that jointly explores inputs and thread schedules. …

Confidential, Attestable, And Efficient Inter-Cvm Communication With Arm Cca, Sina Abdollahi, Amir Al Sadi, Marios Kogias, Hamed Haddadi, David Kotz

Other Faculty Materials

Confidential Virtual Machines (CVMs) are increasingly adopted to protect sensitive workloads from privileged adversaries such as the hypervisor. While they provide strong isolation guarantees, existing CVM architectures lack first-class mechanisms for inter-CVM data sharing due to their disjoint memory model, making inter-CVM data exchange a performance bottleneck in compartmentalized or collaborative multi-CVM systems. Under this model, a CVM's accessible memory is either shared with the hypervisor or protected from both the hypervisor and all other CVMs. This design simplifies reasoning about memory ownership; however, it fundamentally precludes plaintext data sharing between CVMs because all inter-CVM communication must pass through hypervisor-accessible …

Property Testing Ai: An Efficient Frontier, Paul Sopher Lintilhac

Dartmouth College Ph.D Dissertations

In this dissertation, we take a step towards addressing the major problem of a lack of standardized and rigorous approaches to testing and evaluation of AI systems. Taking inspiration from both the fields of Property Testing and Property Based Testing (for programs), we develop a novel taxonomy of partially overlapping classes of properties of AI systems, including simple properties, compound properties, higher order properties, data relation properties, and architecture-utility properties. We argue that this taxonomy categorizes a diverse set of AI traits -- including accuracy, fairness, robustness, monotonicity, point-wise and global privacy properties, sensitivity, and more -- according to the …

Action This Day: The Mathematics And Machinations That Bested The German Enigma, Jonah Weinbaum

Dartmouth College Master’s Theses

This thesis presents a comprehensive and chronological overview of cryptographic techniques designed to break Enigma, beginning in 1932 and culminating in the creation of the Turing-Welchman Bombe. We discuss the mathematical theory and electromechanical implements used to decode one of history's greatest ciphers.

Reexamining the Bombe through the lens of modern group theory, we critique Alan Turing's estimation of the number of "stops" that the Bombe produces for various plaintext-ciphertext pairing structures. To address its limitations, we introduce a new framework for estimating the number of stops by extending John Dixon's theorem concerning the probability that uniformly distributed elements of …

Potsdam: Pareto Optimization Targeting Security, Data, And Mediation, J Peter Brady

Dartmouth College Ph.D Dissertations

Given the growing amount and variety of data handled by modern systems, it is crucial to guarantee the accuracy and protection of input data without errors or malicious intentions. The need to improve security in software programs often conflicts with the assurance of maximum performance, making developers and maintainers hesitant to incorporate more testing.

LangSec (Language-Theoretic Security) is a security approach that treats input validation as a formal language recognition problem, ensuring that only well-defined, unambiguous inputs are processed to eliminate exploitable parsing flaws. This dissertation explores integrating LangSec principles with Pareto optimization to enhance safety and robustness in digital …

A Framework For Evaluating The Security And Privacy Of Smart-Home Devices, And Its Application To Common Platforms, Ravindra Mangar, Timothy Pierson, David Kotz

Dartmouth Scholarship

In this article, we outline the challenges associated with the widespread adoption of smart devices in homes. These challenges are primarily driven by scale and device heterogeneity: a home may soon include dozens or hundreds of devices, across many device types, and may include multiple residents and other stakeholders. We develop a framework for reasoning about these challenges based on the deployment, operation, and decommissioning life cycle stages of smart devices within a smart home. We evaluate the challenges in each stage using the well-known CIA triad—Confidentiality, Integrity, and Availability. In addition, we highlight open research questions at each stage. …