TWC

Recent reports have highlighted incidents of massive Internet traffic interception executed by re-routing Border Gateway Protocol (BGP) paths across the globe (affecting banks, governments, entire network service providers, etc.). The potential impact of these attacks can range from massive eavesdropping to identity-spoofing or selective content modification. In addition, executing such attacks does not require access or proximity to the affected links and networks, posing increasing risks to national security.

Mobile authentication is necessary for preventing unauthorized access to mobile devices with increasingly more private information. Despite significant progress in mobile authentication for sighted people, secure and usable mobile authentication for people with visual impairment remains largely under-explored. This project is to develop, prototype and evaluate novel secure and usable mobile authentication techniques for people with visual impairment.

Software is responsible for many critical government, business, and educational functions. This project aims to develop new methods for finding and repairing some of the most challenging, poorly understood security vulnerabilities in modern software that have the potential to jeopardize the security and reliability of the nation's cyber infrastructure.

Fully homomorphic encryption (FHE) allows an untrusted party to efficiently compute any compact function directly on ciphertexts. When made available over an untrusted cloud server, data is submitted and returned in encrypted form, and the execution remains secure against malicious users. Early FHE proposals had rather disappointing efficiencies. Recently new FHE schemes based on the difficulty of the learning with errors (LWE) problem emerged with orders of magnitude improvement over earlier constructions.

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.