TWC

This project develops the foundations for automating verification of secure and trustworthy systems. It extends the range of analyses that are amenable to automated checking and addresses scalability. Symbolic techniques that represent possibly infinite sets of states by symbolic constraints have become important tools, but many systems of interest fall outside the scope of current techniques.

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.

Data structures have a prominent modern computational role, due to their wide applicability, such as in database querying, web searching, and social network analysis. This project focuses on the interplay of data structures with security protocols, examining two different paradigms: the security for data structures paradigm (SD) and the data structures for security paradigm (DS).

As wireless technologies become more pervasive, it becomes increasingly important for devices to authenticate the locations of other devices. For example, patients with implantable medical devices (IMDs) may reasonably expect that any device used to control their IMD would have to be within arm's reach, to help prevent unauthorized access to their device. In other words, IMDs should enforce policies based on the proximity, and in general the location, of wirelessly connected devices.

Despite rampant criticism of passwords and an abundance of alternative proposals for user authentication (e.g., biometrics), passwords are not likely to be replaced in the near future due to their ease of deployment and familiarity to users. Indeed, while a number of policies for improving password systems have emerged, the most widely adopted of these is to simply increase the size of the space from which passwords are drawn. Even so, for user-chosen secrets, these policies generally make passwords harder to remember and type, leading to user frustration.