TC

This project investigates a new approach for describing and reasoning about security properties of smartphone applications. Smartphones are becoming pervasive, and smartphone applications are increasingly used for a variety of social, health, scientific, and military purposes. However, the capabilities these phones provide, such as access to GPS, camera, Internet, calendar, contacts, and other sensitive information can lead to major security risks. Today's smartphone development methodologies do little to help developers construct applications that safely access sensitive resources.

In the last few years, universally composable (UC) security, defined and extensively investigated by Ran Canetti, has become a popular and important topic in modern cryptography. Canetti's notion has enormous appeal, promising a unified framework under which one can define virtually any cryptographic protocol goal, and further promising that the resulting definitions will be composable in the sense that a protocol solution for some goal will comprise a suitable primitive to use within any other protocol that desires its abstracted functionality.

Freedom of speech is a founding principle of democratic society, and the Internet has become one of the most effective and common means of conveying expression that is likely to be controversial or suppressed. One threat to the freedom of speech online is the now widespread practice of Internet censorship by both private and state interests. These censors use a variety of social and technological means to limit availability or expression of information, stifling the democratic process.

Electronic System Level ( ESL ) designs , specified behaviorally using high-level languages such as SystemC , raise the level of hardware design abstraction . This approach crucially depends on behavioral synthesis , which compiles ESL designs to Register Transfer Level ( RTL ) designs . However , optimizations performed by synthesis tools make their implementation error-prone , undermining the trustworthiness of synthesized hardware. This research develops a mechanized infrastructure for certifying hardware designs generated by behavioral synthesis .

A significant number of attacks on Web browsers and Web applications are successful through the use of malicious inputs. For instance, attacks on web browser extensions target browsers by exploiting vulnerable extensions (add-ons) by supplying malicious input. Malicious inputs exercise unintended behaviors leading to attacks that compromise confidentiality, integrity and availability of web-based systems.