| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 24, 2015 |
| Latest Amendment Date: | July 24, 2015 |
| Award Number: | 1548848 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Nina Amla
namla@nsf.gov (703)292-7991 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2015 |
| End Date: | February 28, 2018 (Estimated) |
| Total Intended Award Amount: | $99,989.00 |
| Total Awarded Amount to Date: | $99,989.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
3227 CHEADLE HALL SANTA BARBARA CA US 93106-0001 (805)893-4188 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
Santa Barbara CA US 93106-5110 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Modern human society relies heavily on web applications and is deeply affected by their poor dependability. Unfortunately, no matter how much effort is put into verification and validation of software, existing techniques are inherently limited, and software is routinely released with bugs and issues that limit its functionality and can dramatically affect the user experience. This project investigates an approach that has the potential to significantly improve the scalability and effectiveness of symbolic program analysis and verification techniques, that will improve the dependability of modern web applications.
This project develops techniques and tools that use symbolic execution and automata-based verification techniques to automatically analyze and verify web applications, and store results of symbolic analyses in a graph database for efficient storage, and retrieval. The methods use incremental and differential analysis strategies that utilize the graph database in order to improve scalability and effectiveness of software analysis and verification. The project trains graduate students, and will make its artifacts publicly available to other researchers and educators.
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.
The main goal of this project was to develop scalable program analysis techniques to improve security and dependability of software systems. Within the scope of this project, we have developed several novel program analysis techniques and improved their scalability.
We developed novel constraint solving and model counting techniques for handling both numeric and string constraints and their combinations. We implemented our results in a novel constraint solver called ABC that stores constraints as automata. To improve scalability of constraint based program analysis, we developed a constraint database called Cashew that can cache numeric and string constraints and model counting queries. We conducted empirical studies that demonstrate that constraint caching can significantly improve the performance of symbolic and quantitative program analyses.
Our results on constraint cashing demonstrate that using appropriate constraint databases, the scalability of symbolic program analysis can be significantly improved.
We developed a novel static, scalable analysis technique for detecting side channels in software systems based on symbolic cost analysis of program paths. We implemented our symbolic path cost analysis technique for detecting side channels in a prototype tool, CoCo-Channel (Compositional Constraint based side Channel analyzer), for analyzing Java programs.
We developed symbolic analysis techniques for detecting vulnerabilities that are due to adaptive side-channel attacks, and synthesizing attacks that exploit the identified vulnerabilities.
Our results on side channel analysis demonstrate that symbolic execution techniques, when combined with automata-based model-counting constraint solvers, can be used to identify side channels in software applications. Side channel analysis is a very important problem in computing since it can be used to identify leakage of privileged information, which is crucial for dependability of modern software systems.
Our results on automated attack synthesis enable us to identify the attacks that malicious users can launch against software systems. This knowledge is necessary for remedying existing vulnerabilities.
We developed a static analysis technique for iOS executables for checking API call vulnerabilities. Using a combination of dependency analysis and string analysis, we were able to detect potential violations of Apple’s API policies (such as restricted use of private/sensitive APIs) in iOS executables.
Our results on information-flow tracking show that it is feasible to perform accurate forensic analysis of attacks in real-world scenarios. This can help making software systems more secure against the increasingly common phenomenon of advanced persistent threats.
The results from the research conducted within the scope of this project were published in international conferences and presented to the international research community. PIs gave invited, distinguished and keynote talks to present the research results they obtained within the scope of this project. The students who participated in this research project have gained valuable research experience and training. They have furthered their education and improved their research skills.
Last Modified: 05/22/2018
Modified by: Tevfik Bultan
Please report errors in award information by writing to: awardsearch@nsf.gov.
