Detail publikace
Flatten and conquer: a framework for efficient analysis of string constraints
Abdulla Parosh
Atig Mohamed (FIT)
Bui Phi Diep (FIT)
Chen Yu-Fang
Rezine Ahmed, Assoc. Prof.
Rummer Philipp
Automata Theory, Formal Verification, String Equation
Popisujeme metodu efektivní analýzi řetězcových omezení založenou na rozplácávání automatů. Používáme metodu zjemňování abstrakce pomocí protipříkladů.
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"
}