Hypertesting of programs : theoretical foundation and automated test generation
Informazioni aggiuntive
Autori
Pasqua M.,
Ceccato M.,
Tonella P.
Tipo
Contributo in atti di convegno
Anno
2024
Lingua
Inglese
Sommario
Hyperproperties are used to define correctness requirements that involve relations between multiple program executions. This allows, for instance, to model security and concurrency requirements, which cannot be expressed by means of trace properties. In this paper, we propose a novel systematic approach for automated testing of hyperproperties. Our contribution is both foundational and practical. On the foundational side, we define a hyper-testing framework, which includes a novel hypercoverage adequacy criterion designed to guide the synthesis of test cases for hyperproperties. On the practical side, we instantiate such framework by implementing HyperFuzz and HyperEvo, two test generators targeting the Non-Interference security requirement, that rely respectively on fuzzing and search algorithms. Experimental results show that the proposed hypercoverage adequacy criterion correlates with the capability of a hypertest to expose hyperproperty violations and that both HyperFuzz and HyperEvo achieve high hypercoverage and high vulnerability exposure with no false alarms (by construction). While they both outperform the state-of-the-art dynamic taint analysis tool Phosphor, HyperEvo is more effective than HyperFuzz on some benchmark programs.
Parole chiave
Search-based testing, Hyperproperties, Information flows, Security testing, Code coverage criteria
Titolo atti di convegno
IEEE/ACM 46th International Conference on Software Engineering (ICSE)
Nome convegno
ICSE '24: IEEE/ACM 46th International Conference on Software Engineering
Luogo convegno
Lisbon Portugal
Data convegno
April 14-24, 2024
Pagine (o numero dell’articolo)
1 - 12
Diffusione
Licenza
CC BY
Visibilità
Pubblico
Status open access
Hybrid
