| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 24, 2015 |
| Latest Amendment Date: | July 24, 2015 |
| Award Number: | 1548856 |
| 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: | $100,000.00 |
| Total Awarded Amount to Date: | $100,000.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
926 DALNEY ST NW ATLANTA GA US 30318-6395 (404)894-4819 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
225 North Ave NW Atlanta GA US 30332-0002 |
| 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.
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 analysistechniques to improve security and dependability of software systems.Within the scope of this project, we have developed several novel programanalysis techniques and improved their scalability.
We developed novel constraint solving and model counting techniques forhandling both numeric and string constraints and their combinations. Weimplemented our results in a novel constraint solver called ABC that storesconstraints as automata. To improve scalability of constraint based programanalysis, we developed a constraint database called Cashew that can cachenumeric and string constraints and model counting queries. We conductedempirical studies that demonstrate that constraint caching can significantlyimprove the performance of symbolic and quantitative program analyses.
Our results on constraint cashing demonstrate that using appropriateconstraint databases, the scalability of symbolic program analysis can besignificantly improved.
We developed a novel static, scalable analysis technique for detectingside channels in software systems based on symbolic cost analysis ofprogram paths. We implemented our symbolic path cost analysis techniquefor detecting side channels in a prototype tool, CoCo-Channel (CompositionalConstraint-based side Channel analyzer), for analyzing Java programs.
We developed symbolic analysis techniques for detecting vulnerabilitiesthat are due to adaptive side-channel attacks, and synthesizing attacks thatexploit the identified vulnerabilities.
Our results on side channel analysis demonstrate that symbolic executiontechniques, when combined with automata-based model-counting constraintsolvers, can be used to identify side channels in software applications. Sidechannel analysis is a very important problem in computing since it can beused to identify leakage of privileged information, which is crucial fordependability of modern software systems.
Our results on automated attack synthesis enable us to identify the attacksthat malicious users can launch against software systems. This knowledgeis necessary for remedying existing vulnerabilities.
We developed a static analysis technique for iOS executables for checkingAPI call vulnerabilities. Using a combination of dependency analysis andstring analysis, we were able to detect potential violations of Apple’sAPI policies (such as restricted use of private/sensitive APIs) in iOSexecutables.
Our results on information-flow tracking show that it is feasible to performaccurate forensic analysis of attacks in real-world scenarios. This canhelp making software systems more secure against the increasingly commonphenomenon of advanced persistent threats.
The results from the research conducted within the scope of this project werepublished in international conferences and presented to the internationalresearch community. PIs gave invited, distinguished and keynote talks topresent the research results they obtained within the scope of this project.
The students who participated in this research project have gained valuableresearch experience and training. They have furthered their education andimproved their research skills.
Last Modified: 05/28/2018
Modified by: Alessandro Orso
Please report errors in award information by writing to: awardsearch@nsf.gov.
