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.
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.
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.
Publications
Yang E
(2013)
Toward Principled Browser Security
in Proceedings of the 14th Workshop on Hot Topics in Operating Systems (HotOS XIV)
Yang E.Z.
(2013)
Toward principled browser security
in 14th Workshop on Hot Topics in Operating Systems, HotOS 2013
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 | 07/2017 |
End | 02/2018 |
Description | VMware Faculty Research Award |
Amount | $20,000 (USD) |
Organisation | VMware, Inc. |
Sector | Private |
Country | United States |
Start | 01/2020 |
End | 12/2020 |
Description | UCL-Stanford Collaboration on Web Browser Security |
Organisation | |
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 | 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 | 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/politicians |
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 |