Hypertesting of programs : theoretical foundation and automated test generation
Additional information
Authors
Pasqua M.,
Ceccato M.,
Tonella P.
Type
Article in conference proceedings
Year
2024
Language
English
Abstract
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.
Keywords
Search-based testing, Hyperproperties, Information flows, Security testing, Code coverage criteria
Conference proceedings
IEEE/ACM 46th International Conference on Software Engineering (ICSE)
Meeting name
ICSE '24: IEEE/ACM 46th International Conference on Software Engineering
Meeting place
Lisbon Portugal
Meeting date
April 14-24, 2024
Pages (or article number)
1 - 12
Diffusion
License
CC BY
Visibility
Public
Status open access
Hybrid
