Program Verification Techniques for Understanding Security Properties of Software

Lead Research Organisation: University College London
Department Name: Computer Science

Abstract

This proposal aims to develop automatic program verification methods that help security engineers to understand software that they have not written themselves. The engineer will be able to make sophisticated queries about resource requirements and temporal behaviour of code, such as about memory safety, privileges, or information flow. Our methods will even support synthesis of behavioural properties for the engineer: rather than make a closed-world assumption, where the complete program and physical computing device are known, our tools will discover logical descriptions of execution environments (preconditons, protocols, invariants, etc.) that pinpoint the assumptions necessary for code safety or those that trigger violations. Such tools would aid engineers by, for example, advising where to concentrate effort when looking for critical security breaches. They would also suggest where to place effort in hardening an application. Finally, by using strong analysis techniques based on verification, guarantees of security properties could be obtained, as well as flaws discovered.

Towards realising this vision we have assembled a team whoseexperience ranges from program verification research on logics and algorithms to systems security research involving new operating system primitives and software structuring principles that achieve robust security goals.

Planned Impact

The work on this proposal will have potential for impact into the industry and the public sector.

We have links into Microsoft, both into static analysis research and into the security division on the product side. The London-based SME Monoidics ltd markets a static analysis tool which would be well placed to be influenced by the theoretical work and analysis prototypes done in this project. We also have a longstanding collaboration with Google on Native Client (NaCl), which securely runs untrusted native code downloaded from the Internet within the Chrome web browser.

These specific connections provide viable avenues for industrial impact of the results of this project. More generally,
static analysis is gaining more attention in industry as time goes on. Major players in avionics, consumer electronics, and the automotive and defence industries use static analysis for bug-catching in-house. Thus, if this project were to achieve its aims there would appear to be opportunity for further industrial impact in the mid- to long-term (.e., 5-10 years and out).

In the public sector, the mere fact of GCHQ's support for the Research Institute in Automatic Program Analysis and Verification indicates interest, and potential for impact. The UK Government has made clear that they view cybersecurity as important, from the Cabinet Office Cybersecurity Strategy document in 2009, through to a parliamentary briefing note "Cybersecurity in the UK" in 2011, to the Cybersecurity Challenge launched in 2012. Generally speaking, as far as the public sector goes, work under this RI call will likely have more avenues for impact into the public sector than static analysis work has had before.
 
Description Today's web developers cobble together JavaScript code from libraries and other web applications written by potentially malicious third parties. The threat to web users' privacy is severe: unbeknownst to either a web application's user or its developer, malicious code included in the application may leak the user's sensitive data to unauthorised third parties. With our collaborators at Mozilla, Google, Stanford, and UCSD, we have designed and built Confinement with Origin Web Labels (COWL), a confinement system for modern web browsers that prevents malicious JavaScript code in web applications from exfiltrating such sensitive data. COWL strengthens privacy for users while also increasing flexibility for application developers: its approach to confinement enables the creation of featureful web applications (e.g., third-party mashups) that are disallowed in the status-quo web.

We have produced implementations of COWL for the Mozilla Firefox and Google Chromium web browsers, and released the former as open source. We have demonstrated the applicability of COWL to a wide range of web applications. We have taken a major first step toward the adoption of COWL in mainstream web browsers by standardising COWL with the World Wide Web Consortium (W3C), the standards body for the web; the First Public Working Draft (FPWD) of COWL was released in October 2015, and our standardisation efforts with the W3C continue. COWL also appeared in USENIX OSDI 2014, the co-premier venue (with ACM SOSP) for computer systems research.

---

Vulnerabilities in modern server-side applications that give rise to sensitive data disclosures arise when programmers make errors: e.g., forgetting to sanitise input from the remote user before executing a dangerous operation with that input, or forgetting to include the appropriate access control check before sending access-controlled data to a remote user. We have designed and built G8, a run-time policy system for the popular Node.js JavaScript development framework for server-side applications. By enforcing security invariants at runtime, G8 blocks unsafe operations and unauthorised disclosures of sensitive information that would otherwise have resulted from programmer errors.

We have produced an implementation of G8 for the Node.js development environment that augments the V8 JavaScript runtime to enforce labeled information flow control-based policies. We have demonstrated that G8 successfully prevents exploits of vulnerabilities in popular server-side Node.js applications, such as the etherpad collaborative text editor.

---

To understand whether or not software may exhibit a specific dangerous (or desirable) behaviour, formal proof of invariants that hold in all the software's possible executions is invaluable. We have devised new formal program analyses and built tools that implement these analyses for real-world program source code.

We have produced analyses and tools that, e.g., prove when an event may happen infinitely often in the future of a program's execution; prove whether fairness is achieved in the execution of a program with infinite branching; and disprove termination of a program through overapproximation.
Exploitation Route COWL may be deployed in mainstream web browsers, for use by the world's web users; our activity to standardise COWL is ongoing.

G8 may be used to secure Node.js server-side applications against attacks that disclose sensitive information to unauthorised parties.

Our program analyses may be used by researchers and practitioners alike to determine whether real-world software exhibits desired security properties.
Sectors Digital/Communication/Information Technologies (including Software)

 
Description Our work on COWL (for web privacy) has led to the creation of a draft standard (First Public Working Draft) with the World Wide Web Consortium (W3C), the body that standardises how the web works (and thus the features included in web browsers, servers, and sites). This standardisation process, which is ongoing at this writing, may eventually lead to the incorporation of COWL into widely used web browsers (e.g., Mozilla Firefox and Google Chrome), and thus to widespread use of COWL to improve privacy for web users.
First Year Of Impact 2015
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Economic

 
Description GCHQ Business Continuity Proposal
Amount £82,083 (GBP)
Funding ID 4196846 
Organisation Government Communications Headquarters (GCHQ) 
Sector Public
Country United Kingdom
Start 08/2017 
End 02/2018
 
Description UCL-Stanford Collaboration on Web Browser Security 
Organisation Google
Department Research at Google
Country United States 
Sector Private 
PI Contribution Collaborated on the design of new privacy techniques for web browsers. Contributed to the research problem definition, design of the privacy techniques, selection of test-case applications, design of experimental evaluation, and writing up of the research in peer-reviewed publications.
Collaborator Contribution Same as the contributions our research team has made; we are equal collaborators on all aspects of the research.
Impact HotOS 2013 paper, Toward Principled Browser Security OSDI 2014 paper, Protecting Users by Confining JavaScript with COWL
Start Year 2013
 
Description UCL-Stanford Collaboration on Web Browser Security 
Organisation Mozilla Research
Country Global 
Sector Charity/Non Profit 
PI Contribution Collaborated on the design of new privacy techniques for web browsers. Contributed to the research problem definition, design of the privacy techniques, selection of test-case applications, design of experimental evaluation, and writing up of the research in peer-reviewed publications.
Collaborator Contribution Same as the contributions our research team has made; we are equal collaborators on all aspects of the research.
Impact HotOS 2013 paper, Toward Principled Browser Security OSDI 2014 paper, Protecting Users by Confining JavaScript with COWL
Start Year 2013
 
Description UCL-Stanford Collaboration on Web Browser Security 
Organisation Stanford University
Country United States 
Sector Academic/University 
PI Contribution Collaborated on the design of new privacy techniques for web browsers. Contributed to the research problem definition, design of the privacy techniques, selection of test-case applications, design of experimental evaluation, and writing up of the research in peer-reviewed publications.
Collaborator Contribution Same as the contributions our research team has made; we are equal collaborators on all aspects of the research.
Impact HotOS 2013 paper, Toward Principled Browser Security OSDI 2014 paper, Protecting Users by Confining JavaScript with COWL
Start Year 2013
 
Description UCL-UCSD collaboration on web security and privacy 
Organisation University of California, San Diego (UCSD)
Department Department of Computer Science and Engineering
Country United States 
Sector Academic/University 
PI Contribution Ongoing design extensions and improvements to the COWL (Confinement with Origin Web Labels) system for web privacy.
Collaborator Contribution Ongoing design extensions and improvements to the COWL (Confinement with Origin Web Labels) system for web privacy.
Impact Not multi-disciplinary; all within Computer Science. No outputs yet.
Start Year 2016
 
Title COWL Confinement Systems for Web Browsers 
Description Implementations of a confinement system to protect users' privacy in the Google Chromium and Mozilla Firefox web browsers. 
Type Of Technology Software 
Year Produced 2014 
Open Source License? Yes  
Impact Early thus far, but press coverage about the code release and research project: http://www.theregister.co.uk/2014/10/07/boffins_build_cowl_web_privacy_system_to_cut_malware_off_at_the_knees/ http://www.engadget.com/2014/10/06/cowl-web-privacy/ http://www.networkworld.com/article/2691741/microsoft-subnet/researchers-unveil-cowl-a-new-system-to-protect-surfers-privacy.html 
URL http://cowl.ws
 
Description Invited talk at Microsoft Research, Redmond, USA 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Received an invitation to give a talk at Microsoft Research in Redmond in the USA on my work on the COWL web browser privacy project. Delivered a 90 minute-long talk (including Q&A) on the design and implementation of the system to influential researchers at Microsoft, including people involved with web security-related products and research at Microsoft.
Year(s) Of Engagement Activity 2015
URL http://research.microsoft.com/apps/video/default.aspx?id=244746&r=1
 
Description Presentation on Browser Privacy to UK Cyber Security Research Conference 2014 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Policymakers/parliamentarians
Results and Impact Presentation led to questions and interest from representatives of the UK government (GCHQ, BIS, OCSIA).

James Quinault, CBE, the head of OCSIA in the UK government, initiated the meeting by citing my research on COWL (the subject of my presentation) as an example of the sort of world-leading technical work on security and privacy that the UK excels at.

After my talk, two representatives from GCHQ asked if I would visit their site and give a longer technical talk on my research on web browser privacy.
Year(s) Of Engagement Activity 2014