Formal methods

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.

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.

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.

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.

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.