UMD

Existing protocol analysis are typically confined to the electronic messages exchanged among computer systems running at the endpoints. In this project we take a broader view in which a protocol additionally encompasses both physical technologies as well as human participants. Our goal is to develop techniques for analyzing and proving security of protocols involving all these entities, with open-audit, remote voting systems such as Remotegrity as our starting point.

Cloud and mobile computing creates new platforms where applications developed by third-party vendors can access users' devices and computer users' private data. Examples include iPhone and Android apps, and cloud-based application marketplaces. This project is a synergistic effort combining social behavioral science and secure software systems design. The first thrust of the project seeks to understand users' privacy expectations for their private data, and how the privacy policies vary in different social contexts.

More appropriate and efficient security solutions against system trespassing incidents can be developed once the attack threat is better understood. However, few empirical studies exist to assess the attack threat. Our proposed research applies "soft science" models (i.e. sociological psychological and criminological) in effort to better understand the threat of system trespassing.

The security of deployed and actively used systems is a moving target, influenced by factors that are not captured in the existing security models and metrics. For example, estimating the number of vulnerabilities in source code does not account for the fact that cyber attackers never exploit some of the discovered vulnerabilities, in the presence of reduced attack surfaces and technologies that render exploits less likely to succeed. Conversely, old vulnerabilities continue to impact security in the wild because some users do not deploy the corresponding software patches.

Hyperproperties [Clarkson and Schneider 2010] can express security policies, such as secure information flow and service level agreements, which the standard kinds of trace properties used in program verification cannot.
Our objective is to develop verification methodologies for hyperproperties.
We intend to apply those methodologies to the construction of secure systems from components with known security properties, thereby addressing the problem of compositional security.