SoS Quarterly Summary Report - UMD - April 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. They have 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. A paper describing these results has been accepted to PLDI 2015 and prior work, published at ICFP'14, was invited to a special issue of the Journal of Functional Programming. The PIs are in the process of launching an interactive web service for experimenting with their system at http://scv.umiacs.umd.edu, and 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 PIs carried out a large-scale measurement of security-patch deployment. They collected a corpus of daily patch-deployment measurements for 1,593 vulnerabilities from 10 popular client applications that are difficult to monitor through network scanning, and are often targeted in spear-phishing attacks. The team found that for 77% of the vulnerabilities analyzed, patching started within 7 days of the disclosure date. But they also observed that none of the applications considered, except for the Chrome browser (which employs automated updates), were able to reach 90% of the vulnerable host population for more than 90% of the patches released during the 5-year observation period. A paper describing this work will accepted for presentation at the IEEE Symposium on Security and Privacy 2015.

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 found 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 co-organized 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 co-chair for CSET: The Workshop on Cyber Security Evaluation and Testing.

Jonathan Katz served as program chair for PKC 2015, and was 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. Vora was invited to participate in the plenary panel: "Blue Skies / Blank Check" at the annual conference of the Election Verification Network (EVN), which is a nonpartisan network of professionals committed to election integrity. Its membership includes "voting activists, computer scientists, election law and voting rights attorneys, academic experts, election officials, civil rights advocates and more."

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.