Collaborative Research: SaTC: CORE: Small: Hyperproperty-based Enforcement of Information-flow Security

Enforcing security policies such as secrecy or integrity is crucial for software systems that handle large volumes of users’ sensitive information, where even a short transient violation of these policies may result in leaking or damaging highly sensitive information, compromising safety, or interruption of vital public or social services. Runtime monitoring and enforcement of security policies remains one of the foundational techniques for securing software systems. Many important security policies such as information-flow policies cannot be expressed as properties of individual executions, but can be expressed as properties on multiple execution traces, which are called hyperproperties. Motivated by a rich set of real-world applications, the overarching objective of this project is to develop effective runtime enforcement techniques for hyperproperties that enable strong protection of systems against various types of cyberattacks and information leaks. This project will bring about a paradigm shift in systematic runtime enforcement of information-flow properties, organized within three research thrusts that will develop novel monitor designs, open-source tools, and perform rigorous evaluation. The first thrust will develop black-box and grey-box predictive monitors for enforcing hyperproperties. This thrust will also investigate different input models, in particular, closed systems where the monitor can manipulate the input to the system to enforce a hyperproperty and reactive systems where the monitor cannot interfere with the input, as it is generated by an uncontrollable environment. The second thrust will focus on developing runtime monitors that are compositional. The project will design a composed monitor infrastructure where parts of the system are guarded by different monitors, as modern systems are composed of heterogeneous components from mutually distrusting sources. The third research thrust is dedicated to rigorous evaluation by delving into applications of the researchers' theoretical findings. This effort will apply results from the first two thrusts to implement monitors to enforce information flow properties and nonmalleable information flow on real world applications. The results of this project are expected to have several advantages as compared to the existing methods: they will be more general, as they can deal with a rich fragment of the temporal logic HyperLTL and will be transferable, compositional, and low-overhead. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.