Detail výsledku
Flatten and conquer: a framework for efficient analysis of string constraints
Abdulla Parosh
Atig Mohamed, FIT (FIT)
Bui Phi Diep
Chen Yu-Fang
Rezine Ahmed, Assoc. Prof.
Rummer Philipp
We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.
Automata Theory, Formal Verification, String Equation
Jak se ukazuje, pro efektivní verifikaci software, zvláště pro analýzu bezpečnosti webových aplikací a podobných programů, psaných ve skriptovacích jazycích jako PHP, JavaScript, ale i v klasických jazycích jako Java nebo C++, je nezbytná technologie pro usuzování o datovém typu řetězec. Naše práce je jednou z mnoha prací vznikajících v poslední době v oblasti analýzy řetězců, které si kladou za cíl navrhnout jazyk pro popis vlastností řetězců pro potřeby analýzy programů, spolu s algoritmy pro řešení řetězcových omezení v něm vyjádřených. Analýza řetězců je náročná proto, že jazyky pro popis řetězcových omezení musejí být jednak velmi expresivní, na hranicích rozhodnutelnosti, a jednak musí být rozhodnutelné velmi efektivně. Proto velkou roli ve hrají heuristiky. Naše práce je založena na poměrně unikátní heuristice, jejíž hlavní myšlenkou je reprezentovat řetězcová omezení jako pomocí takzvaných plochých jazyků. Ploché jazyky jsou omezenější než regulární jazyky, ale dovolují extrémně efektivní reprezentaci a společnou abstrakci regulárních, racionálních, délkových, a dalších řetězcových omezení potřebných v analýze programů. Zároveň v kombinaci se zjemňováním abstrakce založeném na protipříkladech dovolují vyjádřit vlastnosti potřebné v praxi -- jak ukazujeme experimentálně, naše rozhodovací procedura založená na plochých jazycích byla implementována ve volně dostupném nastroji TRAU a dokáže správně vyřešit naprostou většinu relevantních řetězcových omezení vyskytujících se v praxi. Prezentovaný přístup tak reprezentuje radikálně novou a velmi slibnou cestu k prakticky efektivním nástrojům pro řešení řetězcových omezení.
5 citací ve SCOPUS, 12 citací Google Scholar (obojí bez autocitací).
Analýza možných hodnot proměnných typu řetězec je potřebná zejména pro verifikaci a analýzu bezpečnosti webových aplikací, psaných v jazycích jako PHP nebo JavaScript. Tato práce navrhuje jazyk pro popis vlastností řetězců a analýzu jejich platnosti v rámci běhu programu. Jde o výpočetně náročný problém, pro jehož řešení je nutný vývoj efektivních heuristik. Hlavním přínosem zde jsou heuristiky založené na jednoduché a efektivní reprezentaci řetězcových omezení pomocí takzvaných plochých jazyků. Tyto jsou poměrně unikátní v kontextu poměrně velkého množství současně vznikajících řešení. Metoda byla implementována v rámci volně dostupného nástroje TRAU a vykazuje velmi dobré výsledky v kontextu současného stavu poznání.
@inproceedings{BUT146274,
author="Lukáš {Holík} and Parosh {Abdulla} and Mohamed {Atig} and Diep {Bui Phi} and Yu-Fang {Chen} and Ahmed {Rezine} and Philipp {Rummer}",
title="Flatten and conquer: a framework for efficient analysis of string constraints",
booktitle="Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation",
year="2017",
series="ACM",
pages="602--617",
publisher="Association for Computing Machinery",
address="New York",
doi="10.1145/3062341.3062384",
isbn="978-1-4503-4988-8",
url="https://dl.acm.org/citation.cfm?doid=3062341.3062384"
}IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen