Formal methods

group_project

Visible to the public  TWC: Medium: Language-Hardware Co-Design for Practical and Verifiable Information Flow Control

Current cloud computing platforms, mobile computing devices, and embedded devices all have the security weakness that they permit information flows that violate the confidentiality or integrity of information. This project explores an integrated approach in which software and hardware are co-designed with strong, comprehensive, verifiable security assurance. The goal is to develop a methodology for designing systems in which all forms of information flow are tracked, at both the hardware and software levels, and between these levels.

group_project

Visible to the public TWC: Small: Intrusion Detection and Resilience Against Attacks in Cyber and Cyber-Physical Control Systems

This project develops a novel methodology for designing secure cyber and cyber-physical systems that can detect attackers and protect against malicious behavior after the system has been compromised.

group_project

Visible to the public SBE: Small: Statistical Models and Methods for Dynamic Complex Networks

The project examines the structure and function of dynamic networks by formulating and analyzing probabilistic models for temporally evolving networks and processes occurring on them. In addition, the project seeks practical and efficient statistical methods for network inference. The project is primarily motivated by national security concerns surrounding counter-terrorism and cybersecurity, but outcomes should be directly relevant in biological, social, and physical science applications as well as mathematical areas of probability theory, combinatorics, and graph theory.

group_project

Visible to the public STARSS: Small: Self-reliant Field-Programmable Gate Arrays

Field-programmable gate arrays (FPGAs) are hardware circuits that can be reconfigured by a system user after being deployed. FPGAs are a compelling alternative architecture that may allow hardware performance to continue to improve at a dramatic rate. Unfortunately, systems that incorporate an FPGA may allow a potentially untrusted user to reprogram hardware after it has been deployed. Such a scenario enables novel security attacks that can leak a user's private information or corrupt critical information stored on a system, but are performed entirely in hardware.

group_project

Visible to the public TWC: Small: Deker: Decomposing Commodity Kernels for Verification

The problem of insecure computing environments has large impacts on society: security breaches lead to violations of privacy, financial frauds, espionage, sabotage, lost productivity, and more. These, in turn, result in vast economic damage. A major reason for the severity of these consequences is that many systems run on top of an insecure operating system kernel. The Linux kernel, a de facto industry standard for embedded, mobile, cloud, and supercomputing environments, is often a target for security attacks.

group_project

Visible to the public EAGER: Toward Automated Integration of Moving Target Defense Techniques

Moving Target defense (MTD) is a new Cybersecurity paradigm for deterring and disturbing attacks proactively in order to counter the ?asymmetry? phenomena in cyber warfare. A number of moving target techniques have been recently proposed to inverse this asymmetry by randomizing systems? attributes (e.g., configuration) and exhibiting non-determinism to attackers. However, due to potential inter-dependency between various MTD mechanisms, an ad hoc combination of MTD techniques can cause profoundly detrimental effect on security, performance and the operational integrity of the system.

group_project

Visible to the public TWC: Small: Collaborative: Toward Trusted Third-Party Microprocessor Cores: A Proof Carrying Code Approach

Third-party hardware Intellectual Property (IP), written as code in a Hardware Description Language (HDL), is extensively used in modern integrated circuits. Contemporary electronics typically include 75% of third party hardware IP and only 25% in-house design to provide customization or a profit-making edge. Such extensive use of third-party hardware IP in both commercial and military applications raises security and trustworthiness concerns, especially in today's globalized market.

group_project

Visible to the public  TWC: Small: Language-level Control of Authority

Modern computer applications are typically made up of different software components that are created by, or may act on behalf of, mutually distrustful entities. To ensure the security of computer systems, it is important to restrict the ability of the components to perform actions within the computer system. The Principle of Least Authority states that a component should be given only the ability (or authority) it needs to perform its task, and no more.

group_project

Visible to the public TWC: TTP Option: Small: Differential Introspective Side Channels --- Discovery, Analysis, and Defense

Side channels in the security domain are known to be challenging to discover and eliminate systematically. Nevertheless, they can lead to a variety of stealthy attacks seriously compromising cybersecurity. This work focuses on an important class of side channels that are fundamental to the operations of networked systems.

group_project

Visible to the public TWC: Medium: Collaborative: DIORE: Digital Insertion and Observation Resistant Execution

Cloud computing allows users to delegate data and computation to cloud providers, at the cost of giving up physical control of their computing infrastructure. An attacker with physical access to the computing platform can perform various physical attacks, referred to as digital insertion and observation attacks, which include probing memory buses, tampering with memory, and cold-boot style attacks. While memory encryption can prevent direct leakage of data under digital observation, memory access patterns to even encrypted data may leak sensitive information.