CyLab has played a leading role in advancing trustworthy computing systems by developing technologies that make hardware, software, networks, and artificial intelligence more secure, reliable, and resilient. From foundational research on secure architectures, verified systems, and roots of trust to innovations in AI security, privacy engineering, and critical infrastructure protection, CyLab's work helps ensure that the digital systems people rely on every day are worthy of users' trust.

decorative image

Proving Trust Without Hardware

During CyLab’s early years, as the internet became increasingly central to modern life, a group of CyLab researchers helped lay the foundation for a new approach to system security: proving that software running on a device had not been altered, even without relying on specialized security hardware.

Led by Adrian Perrig, their work addressed a fundamental challenge in cybersecurity: how to establish trust in systems that could already be compromised by malicious software.

In 2004, Perrig and CyLab collaborators Arvind Seshadri and Pradeep Khosla joined IBM’s Leendert van Doorn to introduce SWATT (SoftWare-based ATTestation for Embedded Devices), one of the first software-only techniques for remotely verifying the integrity of an embedded device's memory. Rather than requiring trusted hardware, SWATT used a challenge-response protocol and a carefully designed pseudorandom memory traversal to detect unauthorized modifications to a device's software with high probability.

The approach demonstrated that memory attestation could be performed entirely in software, making it practical for resource-constrained and legacy devices ranging from sensor networks to smart appliances.

The team's work expanded in 2005 with “Pioneer: Verifying Code Integrity and Enforcing Untampered Code Execution on Legacy Systems,” authored by Seshadri, Perrig, Khosla, van Doorn, and CyLab researchers Mark Luk and Elaine Shi. Pioneer advanced beyond memory verification by introducing a software-based technique for establishing a dynamic root of trust, and verifying that code executed without tampering on legacy computing platforms.The system showed that verifiable code execution and runtime attestation could be achieved without secure coprocessors or processor extensions, while also demonstrating practical applications, such as detecting kernel rootkits.

Together, SWATT and Pioneer helped establish software-based attestation as a foundational area of systems security research and influenced subsequent work on trusted computing, remote attestation, embedded systems security, and secure execution environments.

Project links:

decorative image

Advancing Secure Computing with Micro-Hypervisors

Throughout our history, CyLab researchers have steadily advanced a vision for securing sensitive applications, even when the underlying operating system cannot be trusted.

The work began in 2009 with TrustVisor, a lightweight micro-hypervisor designed to isolate small, security-critical portions of software from compromised operating systems while enabling remote verification that protected code had not been altered.

Developed by Jonathan McCune, Ning Qu, Yanlin Li, Anupam Datta, Virgil Gligor, and Adrian Perrig, TrustVisor demonstrated that commodity computers could provide strong guarantees of code integrity, data protection, and trustworthy execution without requiring applications or operating systems to be completely rewritten.

Unlike conventional virtualization platforms, TrustVisor dramatically reduced the trusted computing base, making formal verification more practical while preserving compatibility with existing software.

Over the following 15 years, CyLab researchers expanded that foundation into a broader architecture for trustworthy computing. TrustVisor evolved alongside the eXtensible and Modular Hypervisor Framework (XMHF) and new methods for isolating not only processors and memory, but also input/output devices, creating increasingly complete protection for security-sensitive applications.

In 2026, this research culminated in GreenBox, a secure software platform that isolated critical applications from an otherwise unmodified Windows operating system, allowing users to continue running familiar software while executing high-value tasks inside a formally verifiable environment. The GreenBox project was led by Gligor and Miao Yu, whose work explicitly built on the TrustVisor and XMHF research pioneered at Carnegie Mellon. 

GreenBox introduced a user-verifiable mechanism for switching into the protected environment, supported secure applications such as ransomware-resistant cloud file access and trusted remote desktop connections, and was accompanied by an open-source software development kit to encourage broader adoption. By building on years of advances in micro-hypervisors, trusted execution, and formal verification, GreenBox demonstrated a practical path toward deploying high-assurance security on everyday endpoint computers.

TrustVisor and GreenBox represent a long-running CyLab research trajectory: shrinking the amount of software that must be trusted, mathematically verifying critical security components, and making strong system protections practical on commodity hardware. From TrustVisor's first demonstration that sensitive code could execute securely atop an untrusted operating system to GreenBox's modern platform for protecting critical applications against today's increasingly sophisticated cyber threats, CyLab researchers have helped define the evolution of micro-hypervisor technology for trustworthy computing.

Project links:

decorative image

Building Verifiably Secure Systems

CyLab researchers have helped redefine what it means for software to be secure.

Rather than relying solely on testing to discover vulnerabilities after deployment, CyLab research has focused on developing systems that are verifiably secure, where software’s correctness and security can be mathematically proven before it is ever used. For example, CyLab faculty member Bryan Parno and his students have leveraged advances in cryptography, programming languages, and formal methods to lay the foundation for a future in which critical digital infrastructure can provide rigorous security guarantees instead of “best-effort” protection.

A central theme of Parno's research has been securing the software that underpins the modern internet. In 2017, through the international Project Everest research collaboration, Parno and his students helped develop Vale, a framework for mathematically verifying low-level assembly code used in cryptographic software. Their work demonstrated for the first time that verified cryptographic implementations could match or even exceed the performance of traditional implementations while providing formal guarantees of correctness and resistance to common side-channel attacks. The research earned a Distinguished Paper Award at the USENIX Security Symposium and represented a major milestone toward building a verifiably secure HTTPS ecosystem, which protects the vast majority of encrypted internet traffic.

Building on that success, Parno's team helped create EverCrypt in 2019, developing the world's first industrial-strength cryptographic library that is both high performance and mathematically proven to be secure against broad classes of software vulnerabilities. EverCrypt provides guarantees against memory-safety errors, implementation bugs and several of the most common side-channel attacks while maintaining the speed required for real-world deployment.

In 2024, the research team developed Verus, an open-source software verification tool that enables developers to mathematically prove that code written in the Rust programming language is correct, reliable, and secure. Rather than relying solely on testing, Verus converts both a program and its intended behavior into mathematical representations and verifies that the code satisfies its specification for every possible input. By making formal verification faster and more accessible, Verus helps developers eliminate entire classes of software bugs and vulnerabilities before code is deployed.

Several real-world applications have adopted the research team’s code in building their systems. Code from the EverCrypt library has been incorporated into widely used technologies including the Mozilla Firefox web browser, the Python programming language, and Linux kernel's WireGuard VPN, demonstrating that formal verification can scale from academic research to production systems.

Parno and his CyLab collaborators have  fundamentally changed how researchers and industry practitioners think about software assurance. By proving mathematically that critical software behaves as intended, rather than attempting the impossible task of finding every possible bug through testing alone, CyLab researchers have brought the vision of trustworthy digital infrastructure closer to reality.

Project links:

decorative image

Establishing Root of Trust

In the 2010s, CyLab faculty member Virgil Gligor and systems scientist Maverick Woo pursued one of cybersecurity's longest-standing challenges: establishing a trustworthy "root of trust" for computing systems.

A root of trust is the foundational assurance that a computer begins operation in a known, uncompromised state, providing confidence that everything built upon it can also be trusted. Their research sought to move beyond conventional antivirus software and hardware-based trust mechanisms by asking a more fundamental question: can a computer prove that it is free of malware with mathematical certainty?

Their breakthrough came with the paper “Establishing Software Root of Trust Unconditionally,” presented at the 2019 Network and Distributed System Security (NDSS) Symposium, where it received a Distinguished Paper Award. In the paper, Gligor and Woo introduced the first method for establishing a software root of trust without relying on secret cryptographic keys, specialized trusted hardware or assumptions about an attacker's computational capabilities.

Instead, their approach combined detailed knowledge of a system's hardware architecture with truly random inputs and a novel concept known as “space-time optimality” to determine whether malware exists anywhere within a computing device, including inside notoriously difficult-to-inspect device controllers. Their work represented a fundamental advance toward trustworthy computing because it offered a way to detect persistent malware with near certainty rather than relying on signatures or probabilistic detection.

The implications extended well beyond a single malware-detection technique. By demonstrating that a root of trust could be established through rigorous mathematical principles rather than trusted hardware alone, Gligor and Woo challenged decades of assumptions about how secure systems should be designed. Their research opened new directions for provable system integrity, trustworthy boot processes, and resilient computing platforms capable of resisting sophisticated attackers who compromise firmware, device controllers, or other low-level components that traditionally evade detection.

Project links:

decorative image

Protecting the Devices We Rely On Every Day

Since joining CyLab in 2023, Riccardo Paccagnella has been advancing research that reveals hidden weaknesses deep inside the computer chips powering everything from smartphones and laptops to cloud servers. His work focuses on hardware and systems security, uncovering subtle flaws in modern processors that attackers can exploit to steal sensitive information, even when software appears to be secure. By identifying these vulnerabilities and developing practical defenses, Paccagnella's research is helping manufacturers and software developers build more resilient computing systems for billions of users worldwide.

Paccagnella’s research on the Hertzbleed family of attacks has changed how technology companies protect cryptographic software from subtle hardware-based security risks. After Hertzbleed showed that processor power-management features could unintentionally reveal sensitive information, Cloudflare and Microsoft updated cryptographic implementations, while Intel, AMD, and Ampere issued security advisories and Arm and Red Hat revised their guidance. Related work also helped prompt Google to disable certain SVG filters in Chrome and contributed to new industry recommendations for writing more secure cryptographic code.

In 2023, Paccagnella's research team helped expose GPU.zip, a previously unknown side-channel attack that exploited graphics hardware to recover sensitive visual information, prompting security updates across the graphics ecosystem. Two years later, Paccagnella and his collaborators unveiled Pixnapping, a new class of Android attacks capable of secretly capturing information displayed on a device's screen by taking advantage of hardware-level behavior.

The team's GPU.zip and Pixnapping research exposed ways that graphics hardware and software could inadvertently leak sensitive information displayed on a screen. In response to GPU.zip, developers of the widely used Mesa graphics system created a new feature that allows applications to disable potentially risky graphics compression, which was later added to the Khronos OpenGL extension registry. The work also contributed to security changes in Chrome. After Pixnapping showed that malicious Android apps could potentially recover information displayed by other apps, Google released multiple Android patches to address the threat.

Paccagnella has also conducted innovative research on processor prefetching, revealing how performance features designed to make computers faster can also create unexpected security risks. Augury uncovered such behavior in Apple processors, while GoFetch showed that it could be exploited to recover secret cryptographic keys. Paccagnella’s findings led to updates in cryptographic software, operating-system protections, and Apple’s secure-development guidance, while Apple and Intel have introduced controls that can limit this type of processor behavior. His subsequent work on Peek-a-Walk also prompted Intel to update its guidance for protecting systems against related side-channel attacks

Beyond uncovering new attacks, Paccagnella is helping redefine how future computing systems are designed and evaluated for security. His recent work explores how seemingly minor processor optimizations can unintentionally leak confidential data, challenging long-held assumptions about hardware trustworthiness. By combining rigorous analysis with practical mitigation strategies, his research is influencing both industry and academia, ensuring that next-generation processors are built with security as a fundamental design principle rather than an afterthought.

Project links: