Formal methods

group_project

Visible to the public TWC: Small: Using a Capability-Enhanced Microkernel as a Testbed for Language-based Security (CEMLaBS)

This project is investigating the potential for language-based security techniques in the construction of low-level systems software. The specific focus is on the development of an open, capability-enhanced microkernel whose design is based on seL4, a "security enhanced" version of the L4 microkernel that was developed, by a team in Australia, as the first fully verified, general purpose operating system.

group_project

Visible to the public TWC: Small: Scalable Hybrid Attack Graph Modeling and Analysis

Cyber-physical systems (CPSs) operate nearly all of society's critical infrastructures (e.g., energy, transportation and medicine). In performing mission critical functions, CPSs exhibit hybrid (both discrete and continuous) behavior as they use digital technology to control and monitor physical processes. CPS security analysis is particularly challenging because an attacker can make use of a wide variety of vulnerabilities in the digital elements of the system (e.g., the network), the physical elements of the system, or some combination.

group_project

Visible to the public TWC: Small: Automated Protocol Design and Refinement

Online security relies on communication protocols that establish trust and authentication. New protocols are created regularly, such as when Software-as-a-Service companies expose their software through new Web services. In the ideal case, network engineers and protocol experts collaborate to develop a protocol: one responsible for its efficiency and the other for its security. Unfortunately, this ideal is rarely realized.

group_project

Visible to the public STARSS: Small: Collaborative: Practical and Scalable Security Verification of Security-Aware Hardware Architectures

Computers form the backbone of any modern society, and often process large amounts of sensitive and private information. To help secure the software, and the sensitive data, a number of secure hardware-software and processor architectures have been proposed. These architectures incorporate novel protection and defense mechanisms directly in the hardware where they cannot be modified or bypassed, unlike software protections.

group_project

Visible to the public SaTC: STARSS: ICM: Invariant Carrying Machine for Hardware Assurance

Design of complex semiconductor circuits and systems requires many steps, involves hundreds of engineers, and is typically distributed across multiple locations and organizations worldwide. The conventional processes and tools for design of semiconductors can ensure the correctness, that is, the resulting product does what it is supposed to do. However, these processes do not provide confidence about whether the chip is altered such that it provides unauthorized access or control.

group_project

Visible to the public EAGER: Understanding the Strategic Values of Privacy Practices in Organizations

As companies collect consumer data in increasingly larger quantity and mine the data more deeply, trade-offs arise with respect to companies' practices about information privacy. A company may choose practices that augment targeted advertisements or services. However, the financial rewards associated with privacy practices are highly uncertain, since they are affected by a company's competition with rivals.

group_project

Visible to the public EAGER: Cybersecurity Transition To Practice (TTP) Acceleration

The 2011 Federal Cybersecurity Research and Development Plan cites "Accelerating Transition to Practice (TTP)" as one of five strategic objectives in the Cyber Security and Information Assurance (CSIA) Program Component Area. TTP remains a strategic objective of Agencies which fund cybersecurity research, including NSF. However, the NSF cybersecurity portfolio contains only a small amount of security research that has been transitioned into operational activities.

group_project

Visible to the public TWC: Small: Workflows and Relationships for End-to-End Data Security in Collaborative Applications

Access control refers to mechanisms for protecting access to confidential information, such as sensitive medical data. Management of access control policies, in applications that involve several collaborating parties, poses several challenges. One of these is in ensuring that each party in such a collaboration only obtains the minimal set of access permissions that they require for the collaboration. In a domain such as healthcare, it may be critical that access be minimized in this way, rather than allowing all parties equal access to the sensitive information.

group_project

Visible to the public TWC: Small: Memory Analysis and Machine-Code Verification Techniques for Multiprocessor Systems

Due to the ever-increasing complexity of both hardware and software, it is becoming harder to ensure the reliability of high-level programs. The project will develop tools that permit programmers to mechanically verify software via machine-code analysis. The proposed research will similarly advance the science of software analysis, together with the development of rigorous tools capable of performing industrial software verification. The tools are actively being used by industry for hardware specification and analysis.

group_project

Visible to the public TWC: Medium: Collaborative: Scaling and Prioritizing Market-Sized Application Analysis

The emergence of smartphones and more generally mobile platforms as a vehicle for communication, entertainment, and commerce has led to a revolution of innovation. Markets now provide a dizzying array of applications that inform and aid every conceivable human need or desire. At the same time, application markets allow previously unknown multitudes of application developers access to user devices through fast- tracked software publishing with well-documented consequent security concerns.