| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 16, 2014 |
| Latest Amendment Date: | April 20, 2018 |
| Award Number: | 1422471 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Anindya Banerjee
abanerje@nsf.gov (703)292-7885 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2014 |
| End Date: | August 31, 2018 (Estimated) |
| Total Intended Award Amount: | $500,000.00 |
| Total Awarded Amount to Date: | $516,000.00 |
| Funds Obligated to Date: |
FY 2018 = $16,000.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
9500 GILMAN DR LA JOLLA CA US 92093-0021 (858)534-4896 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
9500 Gilman Drive La Jolla CA US 92093-0404 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
Software & Hardware Foundation, Secure &Trustworthy Cyberspace |
| Primary Program Source: |
01001819DB NSF RESEARCH & RELATED ACTIVIT |
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Title: SHF: Small: Refinement Types For Verified Web Frameworks and Applications
Web applications play a crucial role in every aspect of our lives, including banking, commerce, education and healthcare and travel. Despite their importance and ubiquity, they remain notoriously hard to design, develop and deploy as they span several tiers and languages: an HTML/JavaScript client that runs on users' browsers, a central server that implements the application's logic in the "cloud" and a database that stores persistent user data. The goal of this research is to build upon recent advances in SMT-based software verification to develop reliable and secure web frameworks. The intellectual merits of this research are new techniques for specifying and verifying multi-lingual systems spanning databases, scripting languages and service protocols, which are essential ingredients of large software systems. Thus, the project's broader significance and importance is that it will lower the cost of constructing robust web applications, with strong guarantees about the protection of sensitive data about the users' health, finances and other personal information.
To mitigate the impedance mismatch across tiers, developers use web frameworks which have simplified the construction of web applications. However, reliability and security concerns still cut across multiple tiers and languages, making them hard to achieve. This research will use refinement types to specify and verify properties for frameworks and end-to-end safety and security properties for applications. In particular, it will build on the refinement type system of LiquidHaskell, developed in preliminary research, to verify existing frameworks like Haskell's popular SNAP framework, and use it to develop a suite of applications with strong guarantees, thereby showing how the idea can be widely adopted in mainstream frameworks and languages.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
This project supported the development of the LiquidHaskell (LH) system,a language-integrated verifier for the Haskell programming language.
The system allows software engineers to enforce critical correctnessrequirements of their code by closely intertwining types and logicalassertions. As a result, LH empowers developers to specify, criticalproperties including:
- The absence of run-time exceptions,
- Termination,
- Memory safety,
- Data structure invariants,
- Information flow control, and
- Functional correctness
and then to verify, at compile-time, that these requirements hold, no matter how the code is used at run time.
In the limit, developers can write proofs of correctness of arbitrary properties of their code. Unlike specialized proof assistants, LH proofs are simply programs in Haskell, allowing the programmer to take advantage of a mature compiler and an ecosystem of libraries to produce efficient, verified code.
This project directly supported the development of all the key ideas thatare the foundation of the LH system, including the development of:
[1] Sound refinement typing for non-strict languages like Haskell;
[2] Case studies demonstrating how to use LH on real-world libraries;
[3] Bounded quantification as a way to dramatically extend the expressiveness of refinements while preserving decidable checking;
[3] Reflection as means of verifying properties of arbitrary user-defined functions in a complete fashion; and
[4] The Binah and LWeb frameworks for building secure web applications with formal guarantees about the what data is visible to each user.
The tool is developed open-source on Github, and already has a small community of users, with more than 40 users. The project is downloade dabout 50 times a week from github and has been downloaded more than 8000 times from Hackage, the central repository for Haskell libraries.
Several academic groups, including researchers at Carnegie Mellon University, Drexel University, the University of Maryland, and Yale University have used or based their research on LH.
LH has also started to see some industrial adoption, for example,it has been used to verify the memory (pointer) safety of low-levelnetworking code, and of binary serialization libraries.
[1] N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. Peyton-Jones. Refinement Types for Haskell. In ICFP, 2014.
[2] N. Vazou, E. L. Seidel, and R. Jhala. Liquidhaskell: Experience with refinement types in the real world. In ACM SIGPLAN symposium on Haskell, 2014.
[3] N. Vazou, A. Bakst, and R. Jhala. Bounded refinement types. In ICFP, 2015.
[4] N. Vazou, A. Tondwalkar, V. Choudhury, R. G. Scott, R. R. Newton, P. Wadler, and R. Jhala. Refinement reflection: Complete verification with SMT. In POPL, 2018.
[5] J. Parker, N. Vazou, M.W. Hicks. Information flow security for multi-tier web applications. In POPL, 2019.
Last Modified: 01/13/2019
Modified by: Ranjit Jhala
Please report errors in award information by writing to: awardsearch@nsf.gov.
