More Web Proxy on the site http://driver.im/

research-article

Open access

Hypertesting of Programs: Theoretical Foundation and Automated Test Generation

Authors:

Michele Pasqua,

Mariano Ceccato,

Paolo TonellaAuthors Info & Claims

ICSE '24: Proceedings of the IEEE/ACM 46th International Conference on Software Engineering

Article No.: 115, Pages 1 - 12

https://doi.org/10.1145/3597503.3640323

Published: 12 April 2024 Publication History

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.

References

[1]

Allen Troy Acree, Timothy Alan Budd, Richard A. DeMillo, Richard J. Lipton, and Frederick Gerald Sayward. 1979. Mutation Analysis. techreport GIT-ICS-79/08. Georgia Institute of Technology, Atlanta, Georgia.

[2]

Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, and Frédéric Tronel. 2017. Hypercollecting semantics and its application to static analysis of information flow. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18--20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 874--887.

Digital Library

[3]

Thomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider, and Markus Tasch. 2017. RIFL 1.1: A Common Specification Language for Information-Flow Requirements. Technical Report. TU Darmstadt. 46.12.03; LK 01.

[4]

Jonathan Bell and Gail Kaiser. 2014. Phosphor: Illuminating Dynamic Data Flow in Commodity Jvms. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications (Portland, Oregon, USA) (OOPSLA '14). Association for Computing Machinery, New York, NY, USA, 83--101.

Digital Library

[5]

Raven Beutner and Bernd Finkbeiner. 2023. HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems. Log. Methods Comput. Sci. 19, 2 (2023).

[6]

D. W. Binkley and K. B. Gallagher. 1996. Program Slicing. Advances in Computers 43 (1996), 1--50.

[7]

Tegan Brennan, Seemanta Saha, and Tevfik Bultan. 2020. JVM Fuzzing for JIT-Induced Side-Channel Detection. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (Seoul, South Korea) (ICSE '20). Association for Computing Machinery, New York, NY, USA, 1011--1023.

Digital Library

[8]

T. Y. Chen, S. C. Cheung, and S. M. Yiu. 1998. Metamorphic Testing: A New Approach for Generating Next Test Cases. Technical Report. The Hong Kong University of Science and Technology. HKUST-CS98-01.

[9]

David Clark, Sebastian Hunt, and Pasquale Malacaria. 2002. Quantitative Analysis of the Leakage of Confidential Data. Electronic Notes in Theoretical Computer Science 59, 3 (2002), 238--251. QAPL'01, Quantitative Aspects of Programming Laguages (Satellite Event of PLI 2001).

[10]

Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. 2014. Temporal Logics for Hyperproperties. In Principles of Security and Trust, Martín Abadi and Steve Kremer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 265--284.

[11]

M. R. Clarkson and F. B. Schneider. 2010. Hyperproperties. Journal of Computer Security 18, 6 (2010), 1157--1210.

[12]

E. Cohen. 1977. Information Transmission in Computational Systems. Oper. Syst. Rev. 11 (1977), 133--139.

Digital Library

[13]

Kalyanmoy Deb and Himanshu Jain. 2014. An Evolutionary Many-Objective Optimization Algorithm Using Reference-Point-Based Nondominated Sorting Approach, Part I: Solving Problems With Box Constraints. IEEE Transactions on Evolutionary Computation 18, 4 (2014), 577--601.

[14]

Andreas Fellner, Mitra Tabaei Befrouei, and Georg Weissenbacher. 2019. Mutation Testing with Hyperproperties. In Software Engineering and Formal Methods, Peter Csaba Ölveczky and Gwen Salaün (Eds.). Springer International Publishing, Cham, 203--221.

[15]

Jeanne Ferrante, Karl J. Ottenstein, and Joe D. Warren. 1987. The Program Dependence Graph and Its Use in Optimization. ACM Trans. Program. Lang. Syst. 9, 3 (jul 1987), 319--349.

Digital Library

[16]

Bernd Finkbeiner. 2021. Model Checking Algorithms for Hyperproperties (Invited Paper). In Verification, Model Checking, and Abstract Interpretation, Fritz Henglein, Sharon Shoham, and Yakir Vizel (Eds.). Springer International Publishing, Cham, 3--16.

[17]

Tobias Hamann, Mihai Herda, Heiko Mantel, Martin Mohr, David Schneider, and Markus Tasch. 2018. A Uniform Information-Flow Security Benchmark Suite for Source Code and Bytecode. In Secure IT Systems - 23rd Nordic Conference, NordSec 2018, Oslo, Norway, November 28--30, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11252), Nils Gruschka (Ed.). Springer, 437--453.

[18]

Shaobo He, Michael Emmi, and Gabriela Ciocarlie. 2020. ct-fuzz: Fuzzing for Timing Leaks. In 2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST). 466--471.

[19]

Katherine Hough and Jonathan Bell. 2021. A Practical Approach for Dynamic Taint Tracking with Control-Flow Relationships. ACM Trans. Softw. Eng. Methodol. 31, 2, Article 26 (dec 2021), 43 pages.

Digital Library

[20]

T. Hsu, C. Sánchez, and B. Bonakdarpour. 2021. Bounded Model Checking for Hyperproperties. In Tools and Algorithms for the Construction and Analysis of Systems, J. F. Groote and K. G. Larsen (Eds.). Springer International Publishing, Cham, 94--112.

[21]

Johannes Kinder. 2015. Hypertesting: The Case for Automated Testing of Hyperproperties. In 3rd Workshop on Hot Issues in Security Principles and Trust (HotSpot). 1--8.

[22]

G. Le Guernic. 2008. Precise Dynamic Verification of Confidentiality. In Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, Sydney, Australia, August 10--11, 2008 (CEUR Workshop Proceedings, Vol. 372), B. Beckert and G. Klein (Eds.). CEUR-WS.org.

[23]

I. Mastroeni and M. Pasqua. 2018. Verifying Bounded Subset-Closed Hyperproperties. In Static Analysis, Andreas Podelski (Ed.). Springer International Publishing, Cham, 263--283.

[24]

I. Mastroeni and M. Pasqua. 2019. Statically Analyzing Information Flows: An Abstract Interpretation-Based Hyperanalysis for Non-Interference. In Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing. Association for Computing Machinery, 2215--2223.

[25]

Isabella Mastroeni and Michele Pasqua. 2022. Verifying Opacity by Abstract Interpretation. In Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing (Virtual Event) (SAC '22). Association for Computing Machinery, New York, NY, USA, 1817--1826.

Digital Library

[26]

Phil McMinn. 2004. Search-based software test data generation: a survey. Software Testing, Verification and Reliability 14, 2 (2004), 105--156.

[27]

Ibrahim Mesecan, Daniel Blackwell, David Clark, Myra Cohen, and Justyna Petke. 2023. Keeping Secrets: Multi-Objective Genetic Improvement for Detecting and Reducing Information Leakage. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering (ASE '22). Association for Computing Machinery, New York, NY, USA, Article 61, 12 pages.

Digital Library

[28]

I. Mesecan, D. Blackwell, D. Clark, M. B. Cohen, and J. Petke. 2021. HyperGI: Automated Detection and Repair of Information Flow Leakage. In 36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15--19, 2021. IEEE, 1358--1362.

[29]

S. K. Muduli, G. Takhar, and P. Subramanyan. 2020. Hyperfuzzing for SoC Security Validation. In Proceedings of the 39th International Conference on Computer-Aided Design (ICCAD '20). Association for Computing Machinery, New York, NY, USA, 9 pages.

[30]

Shirin Nilizadeh, Yannic Noller, and Corina S. Păsăreanu. 2019. DifFuzz: Differential Fuzzing for Side-Channel Analysis. In Proceedings of the 41st International Conference on Software Engineering (Montreal, Quebec, Canada) (ICSE '19). IEEE Press, 176--187.

Digital Library

[31]

Yannic Noller and Saeid Tizpaz-Niari. 2021. QFuzz: Quantitative Fuzzing for Side Channels. In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (Virtual, Denmark) (ISSTA 2021). Association for Computing Machinery, New York, NY, USA, 257--269.

Digital Library

[32]

Annibale Panichella, Fitsum Meshesha Kifetew, and Paolo Tonella. 2018. Automated Test Case Generation as a Many-Objective Optimisation Problem with Dynamic Selection of the Targets. IEEE Transactions on Software Engineering 44, 2 (2018), 122--158.

[33]

Michele Pasqua, Mariano Ceccato, and Tonella Paolo. 2024. Hypertesting of Programs: Theoretical Foundation and Automated Test Generation (Replication Package). (online).

[34]

Marco Patrignani and Deepak Garg. 2017. Secure Compilation and Hyperproperty Preservation. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 392--404.

[35]

Shubham Sahai, Pramod Subramanyan, and Rohit Sinha. 2020. Verification of Quantitative Hyperproperties Using Trace Enumeration Relations. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 201--224.

[36]

Geoffrey Smith. 2009. On the Foundations of Quantitative Information Flow. In Foundations of Software Science and Computational Structures, Luca de Alfaro (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 288--302.

[37]

Yu Wang, Siddhartha Nalluri, and Miroslav Pajic. 2020. Hyperproperties for Robotics: Planning via HyperLTL. In 2020 IEEE International Conference on Robotics and Automation (ICRA). 8462--8468.

[38]

Mark N. Wegman and F. Kenneth Zadeck. 1991. Constant Propagation with Conditional Branches. ACM Trans. Program. Lang. Syst. 13, 2 (apr 1991), 181--210.

Digital Library

Cited By

Kosorukov IBlackwell DClark DCohen MPetke JFilkov VRay BZhou M(2024)Mining for Mutation Operators for Reduction of Information Flow Control ViolationsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695308(2324-2328)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695308

Index Terms

Hypertesting of Programs: Theoretical Foundation and Automated Test Generation
1. Security and privacy
  1. Systems security
    1. Information flow control
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Achieving scalable mutation-based generation of whole test suites

Without complete formal specification, automatically generated software tests need to be manually checked in order to detect faults. This makes it desirable to produce the strongest possible test set while keeping the number of tests as small as ...
A detailed investigation of the effectiveness of whole test suite generation

A common application of search-based software testing is to generate test cases for all goals defined by a coverage criterion (e.g., lines, branches, mutants). Rather than generating one test case at a time for each of these goals individually, whole ...
Mutation-based test generation for quantum programs with multi-objective search
GECCO '22: Proceedings of the Genetic and Evolutionary Computation Conference

Mutation testing is often used for designing new tests, and involves changing a program in minor ways, which results in mutated versions of the program, i.e., mutants. An effective test suite should find faults (or kill mutants) with a minimum number of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '24: Proceedings of the IEEE/ACM 46th International Conference on Software Engineering

May 2024

2942 pages

ISBN:9798400702174

DOI:10.1145/3597503

Co-chairs:
Ana Paiva,
Rui Abreu,
Program Co-chairs:
Abhik Roychoudhury,
Margaret Storey

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

In-Cooperation

Faculty of Engineering of University of Porto

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 April 2024

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

ICSE '24

Sponsor:

SIGSOFT

ICSE '24: IEEE/ACM 46th International Conference on Software Engineering

April 14 - 20, 2024

Lisbon, Portugal

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
336
Total Downloads

Downloads (Last 12 months)336
Downloads (Last 6 weeks)64

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kosorukov IBlackwell DClark DCohen MPetke JFilkov VRay BZhou M(2024)Mining for Mutation Operators for Reduction of Information Flow Control ViolationsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695308(2324-2328)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695308

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents