Researchers have developed gate-level information flow tracking (GLIFT) technology that allows security analysis to be done on both hardware and software together. The GLIFT technology also allows security properties to be formalized as assertions that are verifiable at design time and allows properties such as non-interference to be proven formally for time-sensitive hardware/software systems. By providing the tools necessary to identify and control undesirable flows of information (such as those that might be injected by an adversary) at the level of hardware, the GLIFT technology captures some of the most insidious and difficult to anticipate security problems. Ultimately this makes it possible to more tightly integrate computing systems from different levels of security in a reliable manner, reducing replication (decreasing size and power), and making system-level evaluation cheaper and faster. Specifically, GLIFT technology provides the capacity of ensuring that a specified subset of inputs could never affect a specified subset of outputs.
The GLIFT technology may transform the design of secure and trustworthy computer systems by providing a methodology that allows formal security properties to be tested and verified. It can be used to analyze systems for potential faults and vulnerabilities, as a way to ensure design constraints are understood both software and hardware designers (whom often have no formal security training), and to guide the redesign of those systems to insure such problems no longer exist. It is an enabling technology that allows engineers to efficiently build critical systems, that helps protects users and the general public from damaging events, and ensures that the notion of formal properties are treated a first-order design constraint by the practicing computer system engineers. Researchers believe our technology has the ability create the skills and tools that future embedded hardware and software engineers will need to evaluate the trustworthiness of their systems, and that it will ease the development of those critical systems that we all depend on for our safety and livelihood.
The intellectual merit of this project focused on understanding the commercial viability of technology related to securing hardware and software systems. This technology was developed under previous NSF grant in PI Kastner’s research group. The technology enables computer system designers to specify intended security properties of applications running on the system under development. The technology will test and/or verify whether these security properties are maintained, and provide an example situation when they property is violated. Example properties include: "Does the secret information (e.g., credit card or personal data) ever leak to an untrusted piece of software?", and "Can the radio (or other low integrity portion of the system) ever affect the braking system (or other high integrity part of the system) in an automobile?". Over the course of this project, we met with over 120 potential customers and partners to assess the viability of our technology. Furthermore, we received training on the best ways to develop a business plan and viable initial product. The broader impact of this project revolves around creation of a startup company, Tortuga Logic, which was formed shortly after the end of the I-Corps program. This company currently has four employees who are focused on creating technology that makes systems more secure, and developing novel systems in a variety of different high assurance markets (e.g,. automotive, medical devices, and avionics). These systems must be formally verified to adhere to strict properties related to confidentiality and integrity. It is important to secure these systems as they are critical to our national infrastructure, and they are responsible for the safety and health of billions of people around the world.
