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

research-article

Synthesis of infinite-state systems with random behavior

Authors:

Grigory Fedyukovich,

Sanjai Rayadurgam,

Michael W. WhalenAuthors Info & Claims

ASE '20: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering

Pages 250 - 261

https://doi.org/10.1145/3324884.3416586

Published: 27 January 2021 Publication History

Abstract

Diversity in the exhibited behavior of a given system is a desirable characteristic in a variety of application contexts. Synthesis of conformant implementations often proceeds by discovering witnessing Skolem functions, which are traditionally deterministic. In this paper, we present a novel Skolem extraction algorithm to enable synthesis of witnesses with random behavior and demonstrate its applicability in the context of reactive systems. The synthesized solutions are guaranteed by design to meet the given specification, while exhibiting a high degree of diversity in their responses to external stimuli. Case studies demonstrate how our proposed framework unveils a novel application of synthesis in model-based fuzz testing to generate fuzzers of competitive performance to general-purpose alternatives, as well as the practical utility of synthesized controllers in robot motion planning problems.

References

[1]

[n.d.]. Peach fuzzer. https://www.peach.tech/.

[2]

Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. 2017. Automated formal synthesis of digital controllers for state-space physical plants. In International Conference on Computer Aided Verification. Springer, 462--482.

[3]

Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. IEEE, 1--8.

[4]

Cornelius Aschermann, Tommaso Frassetto, Thorsten Holz, Patrick Jauernig, Ahmad-Reza Sadeghi, and Daniel Teuchert. 2019. NAUTILUS: Fishing for Deep Bugs with Grammars. In NDSS.

[5]

Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England), Vol. 13. 14.

[6]

Tewodros Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. 2014. A constraint-based approach to solving games on infinite graphs. In POPL. ACM, 221--233.

[7]

Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. 2014. A constraint-based approach to solving games on infinite graphs. In POPL. ACM, 221--234.

[8]

Nikolaj Bjørner and Mikolás Janota. 2015. Playing with Quantified Satisfaction. In LPAR (short papers) (EPiC Series in Computing), Vol. 35. EasyChair, 15--27.

[9]

Marcel Böhme, Van-Thuan Pham, and Abhik Roychoudhury. 2017. Coverage-based greybox fuzzing as markov chain. IEEE Transactions on Software Engineering 45, 5 (2017), 489--506.

[10]

Patricia Bouyer, Marie Duflot, Nicolas Markey, and Gabriel Renault. 2009. Measuring permissivity in finite games. In International Conference on Concurrency Theory. Springer, 196--210.

Digital Library

[11]

Supratik Chakraborty, Dror Fried, Lucas M Tabajara, and Moshe Y Vardi. 2018. Functional synthesis via input-output separation. In 2018 Formal Methods in Computer Aided Design (FMCAD). IEEE, 1--9.

[12]

Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. 2016. The Kind 2 model checker. In International Conference on Computer Aided Verification. Springer, 510--517.

[13]

Koen Claessen, Jonatan Kilhamn, Laura Kovács, and Bengt Lennartson. 2017. A Supervisory Control Algorithm Based on Property-Directed Reachability. In Haifa Verification Conference. Springer, 115--130.

[14]

Grigory Fedyukovich and Aarti Gupta. 2019. Functional Synthesis with Examples. In CP (LNCS), Vol. 11802. Springer, 547--564.

[15]

Grigory Fedyukovich, Arie Gurfinkel, and Aarti Gupta. 2019. Lazy but Effective Functional Synthesis. In VMCAI (LNCS), Vol. 11388. Springer, 92--113.

[16]

Grigory Fedyukovich, Arie Gurfinkel, and Natasha Sharygina. 2015. Automated Discovery of Simulation Between Programs. In LPAR (LNCS), Vol. 9450. Springer, 606--621.

[17]

Bernd Finkbeiner. 2016. Synthesis of Reactive Systems. Dependable Software Systems Engineering 45 (2016), 72--98.

[18]

Dustin Fraze. [n.d.]. The DARPA Cyber Grand Challenge. https://www.darpa.mil/program/cyber-grand-challenge.

[19]

Daniel J Fremont, Alexandre Donzé, and Sanjit A Seshia. 2017. Control improvisation. arXiv preprint arXiv:1704.06319 (2017).

[20]

Daniel J. Fremont and Sanjit A. Seshia. 2018. Reactive Control Improvisation. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 307--326.

[21]

Andrew Gacek, John Backes, Mike Whalen, Lucas Wagner, and Elaheh Ghassabani. 2018. The JKind Model Checker. In International Conference on Computer Aided Verification. Springer, 20--27.

[22]

Andrew Gacek, Andreas Katis, Michael W Whalen, John Backes, and Darren Cofer. 2015. Towards Realizability Checking of Contracts Using Theories. In NFM (LNCS), Vol. 9058. Springer, 173--187.

[23]

Enric Galceran and Marc Carreras. 2013. A survey on coverage path planning for robotics. Robotics and Autonomous systems 61, 12 (2013), 1258--1276.

[24]

Sumit Gulwani. 2010. Dimensions in program synthesis. In PPDP. ACM, 13--24.

[25]

Christian Holler, Kim Herzig, and Andreas Zeller. 2012. Fuzzing with code fragments. In Presented as part of the 21st {USENIX} Security Symposium ({USENIX} Security 12). 445--458.

[26]

Falk Howar and Bernhard Steffen. 2018. Active automata learning in practice. In Machine Learning for Dynamic Software Analysis: Potentials and Limits. Springer, 123--148.

[27]

Erwan Jahier, Pascal Raymond, and Nicolas Halbwachs. [n.d.]. The Lustre V6 Reference Manual. http://www-verimag.imag.fr/Lustre-V6.html.

[28]

Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, and Michael W Whalen. 2018. Validity-guided synthesis of reactive systems from assume-guarantee contracts. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 176--193.

[29]

Andreas Katis, Andrew Gacek, and Michael W Whalen. 2015. Machine-Checked Proofs For Realizability Checking Algorithms. In VSTTE. Springer, 110--123.

[30]

Andreas Katis, Andrew Gacek, and Michael W Whalen. 2016. Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. In FormaliSE. IEEE, 36--41.

[31]

George Klees, Andrew Ruef, Benji Cooper, Shiyi Wei, and Michael Hicks. 2018. Evaluating fuzz testing. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. 2123--2138.

Digital Library

[32]

Bettina Könighofer, Mohammed Alshiekh, Roderick Bloem, Laura Humphrey, Robert Könighofer, Ufuk Topcu, and Chao Wang. 2017. Shield synthesis. Formal Methods in System Design 51, 2 (2017), 332--361.

Digital Library

[33]

Newton Lee. 2015. DARPA's Cyber Grand Challenge (2014--2016). In Counterterrorism and Cybersecurity. Springer, 429--456.

[34]

Valentin Jean Marie Manès, HyungSeok Han, Choongwoo Han, Sang Kil Cha, Manuel Egele, Edward J Schwartz, and Maverick Woo. 2019. The art, science, and engineering of fuzzing: A survey. IEEE Transactions on Software Engineering (2019).

[35]

Daniel Neider and Oliver Markgraf. 2019. Learning-based synthesis of safety controllers. In 2019 Formal Methods in Computer Aided Design (FMCAD). IEEE, 120--128.

[36]

Daniel Neider and Ufuk Topcu. 2016. An automaton learning approach to solving safety games over infinite graphs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 204--221.

Digital Library

[37]

ThanhVu Nguyen, Westley Weimer, Deepak Kapur, and Stephanie Forrest. 2017. Connecting program synthesis and reachability: Automatic program repair using test-input generation. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 301--318.

[38]

Hui Peng, Yan Shoshitaishvili, and Mathias Payer. 2018. T-Fuzz: fuzzing by program transformation. In 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 697--710.

[39]

Van-Thuan Pham, Marcel Böhme, and Abhik Roychoudhury. 2016. Model-based whitebox fuzzing for program binaries. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering. 543--553.

Digital Library

[40]

Michael Rash. [n.d.]. afl-cov - AFL Fuzzing Code Coverage. https://github.com/mrash/afl-cov.

[41]

Sanjay Rawat, Vivek Jain, Ashish Kumar, Lucian Cojocar, Cristiano Giuffrida, and Herbert Bos. 2017. VUzzer: Application-aware Evolutionary Fuzzing. In NDSS, Vol. 17. 1--14.

[42]

Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur, and Gernot Heiser. 2009. Automatic device driver synthesis with Termite. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. ACM, 73--86.

Digital Library

[43]

Mohammad Reza Shoaei, Laura Kovács, and Bengt Lennartson. 2014. Supervisory control of discrete-event systems via IC3. In Haifa Verification Conference. Springer, 252--266.

[44]

Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In NDSS, Vol. 16. 1--16.

[45]

Mark Utting, Alexander Pretschner, and Bruno Legeard. 2012. A taxonomy of model-based testing approaches. Software testing, verification and reliability 22, 5 (2012), 297--312.

[46]

Spandan Veggalam, Sanjay Rawat, Istvan Haller, and Herbert Bos. 2016. Ifuzzer: An evolutionary interpreter fuzzer using genetic programming. In European Symposium on Research in Computer Security. Springer, 581--601.

[47]

Michal Zalewski. [n.d.]. American Fuzzy Lop. https://lcamtuf.coredump.cx/afl/.

Cited By

Rodríguez ASánchez C(2024)Realizability Modulo TheoriesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100971(100971)Online publication date: May-2024
https://doi.org/10.1016/j.jlamp.2024.100971
Hu MXia JZhang MChen XMallet FChen M(2023)Automated Synthesis of Safe Timing Behaviors for Requirements Models Using CCSLIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.328541242:12(5127-5140)Online publication date: Dec-2023
https://doi.org/10.1109/TCAD.2023.3285412

Recommendations

Random pattern testable logic synthesis
ICCAD '94: Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design

Previous procedures for synthesis of testable logic guarantee that all faults in the synthesized circuits are detectable. However, the detectability of many faults in these circuits can be very low leading to poor random pattern testability. A new ...
System Synthesis with VHDL: A Transformational Approach
Can reactive synthesis and syntax-guided synthesis be friends?
SPLASH Companion 2021: Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '20: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering

December 2020

1449 pages

ISBN:9781450367684

DOI:10.1145/3324884

General Chair:
John Grundy,
Program Chairs:
Claire Le Goues,
David Lo

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 January 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

United States Department of the Navy, Office of Naval Research

Conference

ASE '20

Sponsor:

ASE '20: 35th IEEE/ACM International Conference on Automated Software Engineering

December 21 - 25, 2020

Virtual Event, Australia

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
76
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)2

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Rodríguez ASánchez C(2024)Realizability Modulo TheoriesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100971(100971)Online publication date: May-2024
https://doi.org/10.1016/j.jlamp.2024.100971
Hu MXia JZhang MChen XMallet FChen M(2023)Automated Synthesis of Safe Timing Behaviors for Requirements Models Using CCSLIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.328541242:12(5127-5140)Online publication date: Dec-2023
https://doi.org/10.1109/TCAD.2023.3285412

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents