Fakulta informačních technologií VUT v Brně

Detail publikace

Flatten and conquer: a framework for efficient analysis of string constraints

ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed a RUMMER Philipp. Flatten and conquer: a framework for efficient analysis of string constraints. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM. New York: Association for Computing Machinery, 2017, s. 602-617. ISBN 978-1-4503-4988-8. Dostupné z: https://dl.acm.org/citation.cfm?doid=3062341.3062384
Název česky
Rozplácni a panuj: efektivní analýza řetězcových omezení
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Abdulla Parosh A. (Uppsala)
Atig Mohamed F. (Uppsala)
Bui Phi Diep (Uppsala)
Holík Lukáš, Mgr., Ph.D. (UITS FIT VUT)
Chen Yu-Fang (ASIN)
Rezine Ahmed (LIU)
Rummer Philipp (Uppsala)
URL
Abstrakt
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ů. 
Popis doplnění
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í).
Popis - stručný
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í.
Rok
2017
Strany
602-617
Sborník
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation
Řada
ACM
Konference
ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelona, ES
ISBN
978-1-4503-4988-8
Vydavatel
Association for Computing Machinery
Místo
New York, US
DOI
BibTeX
@INPROCEEDINGS{FITPUB11577,
   author = "A. Parosh Abdulla and F. Mohamed Atig and Diep Phi Bui and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and Ahmed Rezine and Philipp Rummer",
   title = "Flatten and conquer: a framework for efficient analysis of string constraints",
   pages = "602--617",
   booktitle = "Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation",
   series = "ACM",
   year = 2017,
   location = "New York, US",
   publisher = "Association for Computing Machinery",
   ISBN = "978-1-4503-4988-8",
   doi = "10.1145/3062341.3062384",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11577"
}
Nahoru