SoS Quarterly Summary Report - UMD - January 2015

Lablet Summary Report
Purpose: To highlight progress. Information is generally at a higher level which is accessible to the interested public.

A). Fundamental Research
The UMD lablet involves several projects looking at different aspects of the five hard problems.

Clarkson and Hicks are attacking the problem of compositional security by trying to develop a verification methodology based on hyperproperties, a generalization of the classical notion of properties. This methodology, if successful, would enable verification that software systems satisfy security policies, thus providing predictable security and increasing the trustworthiness of software. It would, in particular, allow program components to be analyzed independently and then securely composed to build larger systems in a scalable fashion.

Clarkson has recently been working on an automated verification methodology for security. In this methodology, security policies are expressed as logical formulas, and a model checker verifies those formulas. The formulas are expressed in a new logic named HyperLTL, which generalizes linear-time temporal logic (LTL). A paper on this work was published at the Conference on Principles of Security and Trust, 2014.

Van Horn et al. are investigating compositional verification techniques using language-based mechanisms for specifying and enforcing program properties called contracts. Initial results confirm that behavioral properties of programs can be verified using this approach and they are now trying to scale the approach to cover multi-language programs and security properties. This team recently made a theoretical breakthrough by showing how to efficiently generate counterexamples witnessing contract violations. This is important for testing and debugging software that uses contracts. They have been able to prove that their method is both sound and relatively complete. They are currently in the process of launching an interactive web service for experimenting with the system at http://scv.umiacs.umd.edu/. They plan to advertise the service widely to the PL community in the coming months.

Dumitras et al. are working to design more-informative metrics to quantify security of deployed systems. This work addresses the hard problem of developing quantifiable metrics for assessing the security of systems, and understanding how those metrics evolve in the real world. The research team has formalized several security metrics derived from field data, including the count of vulnerabilities exploited and the size of the attack surface actually exercised in real-world attacks, and evaluated these metrics on nearly 300 million reports of intrusion-protection telemetry, collected on more than six million hosts. They have found several interesting results so far, including: (1) The exploitation ratio and the exercised attack surface tend to decrease with newer product releases. (2) Hosts that quickly upgrade to newer product versions tend to have a reduction in exercised attack surfaces. (3) Quantitative improvements with respect to the metrics they have studied are often associated with the introduction of new security technologies, thus demonstrating the effectiveness of those technologies in the field. A paper on this work was published at RAID 2014.

Subrahmanian et al. are using an empirical approach to study factors that affect the rate at which security patches are deployed. A longer-term goal is to correlate this data with sociological studies of network administrators, to determine why patches are not deployed more quickly. This work addresses, in part, the hard problem of developing quantifiable metrics for assessing the security of systems, and understanding how those metrics evolve in the real world. As an example, the team has conducted a study to determine how SSL certificates were reissued and revoked in response to a widespread vulnerability, Heartbleed, that enabled undetectable key compromise. They conducted large-scale measurements and developed new methodologies to determine how the most-popular 1 million web sites reacted to this vulnerability in terms of certificate management, and how this impacts security for clients that use those web sites. They found that the vast majority of vulnerable certificates had not been reissued; further, of those domains that reissued certificates in response to Heartbleed, 60% did not revoke their vulnerable certificates. A paper on this work was published in the Proceedings of the ACM Internet Measurement Conference, 2014.

Cukier and Maimon are applying a criminological viewpoint to develop a better understand attackers' behavior. Using honeypots deployed at the University of Maryland, they are studying how different system-level aspects affect intruders' behavior. The main accomplishement of this quarter is a submission to DSN reporting on their study using data collected over 31 months from two target computer configurations: one presenting attackers with a warning banner, and one that does not. They observed significant (p<0.05) differences based on country-of-origin of the attacker, and also found that the use of a banner altered behavior originating in China.

Aviv and Golbeck are focusing on using empirical studies (surveys) to understand users' perceptions of security and usability. The pverarching goal is to apply what they learn to predict user perceptions, and to use those predictions to design better policies, better user interfaces, and more-secure systems generally. This would enable the design of systems in which users' perceptions of security match some known metric of security, thus inducing security by design. In one recent work, they have studied perceptions of security and usability for Android's graphical password mechanism. They found that users' perceptions of security are unaffected by spatial shifting, but greatly affected by "complexity." Most surprisingly, they were able to predict perceptions and foundnd that none of the tested features alone impacted perceptions, but rather the total length of the password was the most predictive of security perceptions. A paper on this topic was accepted to ACSAC 2014.

Shilton et al. have begun undertaking qualitative studies of users and developers in an effort to discover factors that encourage or discourage privacy and security by design. This work is directed at the broader goal of understanding human behavior and its impact on security. They have continued interviews with mobile application developers focused on cultural and workplace dynamics, and these are expected to progress over the course of the coming year. They are also working on contextual privacy software whose goal is to make information sharing more transparent and user-friendly.

Baras and Golbeck are studying the fundamental notion of trust, and seeking to develop appropriate models that can be applied to study the dynamics of small groups of parties exploring mechanisms for collaboration based on their local policies. They have used game theory to characterize the costs and benefits of collaboration as a function of the level of trust, and have proved formally the conjecture that "trust is a lubricant for cooperation." This work directly addresses the hard problem of policy-governed secure collaboration, among others.

Katz and Vora have adapted a protocol for remote electronic voting based on physical objects like scratch-off cards. What is particularly novel here is that the human voter is explicitly modeled as a participant in the protocol, taking into account limitations on the kinds of computations humans can be expected to perform. In this sense, this work related to the general problem of modeling human behavior and appropriately taking human behavior into account when designing security protocols.

B). Community Interaction

Tudor Dumitras and Jonathan Katz organized a 2-day workshop on "data-driven security" to which all lablet members were invited. Researchers from outside the lablet also attended. See http://www.umiacs.umd.edu/~tdumitra/data-driven for further information.

Jennifer Golbeck and co-authors submitted a survey paper to IEEE Security & Privacy, covering the "human behavior" hard problem.

David Van Horn's results on contract verification were presented at the National Institute of Informatics special meeting on "Software Contracts for Communication, Monitoring, and Security, as well as a Dagstuhl seminar on analysis and verification. The results were also presented at the ACM SIGPLAN conference on functional programming. The presentation of the ICFP 2014 paper was recorded and made available on YouTube; it has been circulated among the programming language community.

Elaine Shi is co-organizing the NSF SATC PI meeting to take place in January 2015. She is also serving as program co-chair for ICICS and the AsiaCCS-SCC workshop.

Adam Aviv is serving as program chair for CSET: The Workshop on Cyber Security Evaluation and Testing.

Jonathan Katz is serving as program chair for PKC 2015, and is also on the program committee for the 2015 IEEE Security & Privacy Conference.

A paper by Elaine Shi and Michael Hicks was selected as the winner of the NSA's second annual "Best Scientific Cybersecurity Paper" Competition.

Michael Hicks ran a "Build It, Break It, Fix It" context which drew the interest of students from 61 universities from across the U.S., including 39 students from the University of Maryland. In contrast to security competitions which encourage teams only to attack systems and find vulnerabilities, the goal of this contest is to encourage writing of secure programs in the first place.

Michael Hicks is serving as program chair for the 2015 Computer Security Foundations Workshop, and is also on the program committee for the 2015 IEEE Security & Privacy Conference. He also serves on the IDA/CCS program review committee. He has been blogging about programming-language security at pl-enthusiast.net

Poorvi Vora is on the technical team for the end-to-end verifiable internet voting project of the Overseas Vote Foundation, the largest organization providing services to overseas US voters. Michael Clarkson is ont he advisory council for this project.

John Baras gave an invited keynote lecture on "Security and Trust in a Networked World" at the Workshop on Security and Safety: Issues, Concepts, and Ideas in Athens, Greece.

C). Educational

Michael Hicks, Jen Golbeck, and Jonathan Katz are offering computer-security MOOCs on Coursera. These courses will cover programming-langauge security, cryptography, and usable security.

Adam Aviv sponsored a female high-school student for an 8-week internship. He is also developing a senior-level elective on cybersecurity, as well as one focusing on usable security.

David Van Horn has incorporated his work into his graduate class on "Program Analysis and Understanding." He will also work to incorporate this into the pedagogically oriented programming environment accompanying his textbook "How to Design Programs." He was invited to lecture about his work at a graduate summer school at the University of Utah in July.

Katie Shilton has developed a module focusing on the human side of implementing security that will be incorporated into two courses: a Masters-level course on "Policy Issues on Digital Curation" and a post-graduate course on the same topic. She will be incorporating her findings from her current research into this module. A project based on the "Bubbles" work is being incorporated into a mobile-development undergraduate course offered this semester.

Tudor Dumitras is offering a course on distributed-systems security that incorporates a discussion of security metrics and empirical studies of security properties.

Michel Cukier leads the ACES undergraduate honors program in cybersecurity, which incorporates a holistic approach to cybersecurity covering technical, policy, and behavioral aspects of the problem.