Funded Projects

Security is an important aspect of software systems with which we interact daily. Achieving security and preventing abuse of an application requires addressing multiple key aspects. First, the underlying cryptographic techniques and other security protection mechanisms must provide adequate protection against adversarial behavior. Second, the system must be properly configured to enforce the necessary protection mechanisms. Third, the software needs to be correctly invoked by the end users to avoid misuse of personal data and computing resources. These aspects are not simultaneously taken into account in current system design, which brings motivation to this work. In this project, we aim to develop a holistic model that formally reasons about the security properties, system guarantees, and human behavior of a system at large. In particular, it is possible to formally show that security mechanisms meet their expected security objectives. It is also possible to develop a formal model of a software system and formally prove it meets specific guarantees. Similarly, formal modeling can be used to characterize human behavior, including in security contexts. The goal of this project is to combine these disconnected components into a single unified model that will allow us to formally reason about the safe use of a software system that provably meets its security guarantees.