Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2018: Static Analysis pp 71–76Cite as

New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11002))

Abstract

The main goal of software synthesis is to automatically derive code from a given specification. The specification can be either explicitly written, or specified through a couple of representative examples illustrating the user’s intent. However, sometimes there is no specification and we need to infer the specification from a given environment. This paper present two such efforts.

We first show, using verification for configuration files, how to learn specification when the given examples is actually a set of configuration files. Software failures resulting from configuration errors have become commonplace as modern software systems grow increasingly large and more complex. The lack of language constructs in configuration files, such as types and grammars, has directed the focus of a configuration file verification towards building post-failure error diagnosis tools. We describe a framework which analyzes data sets of correct configuration files and derives rules for building a language model from the given data set. The resulting language model can be used to verify new configuration files and detect errors in them.

We next describe a systematic effort that can automatically repair firewalls, using the programming by example approach. Firewalls are widely employed to manage and control enterprise networks. Because enterprise-scale firewalls contain hundreds or thousands of policies, ensuring the correctness of firewalls – whether the policies in the firewalls meet the specifications of their administrators – is an important but challenging problem. In our approach, after an administrator observes undesired behavior in a firewall, she may provide input/output examples that comply with the intended behavior. Based on the given examples, we automatically synthesize new firewall rules for the existing firewall. This new firewall correctly handles packets specified by the examples, while maintaining the rest of the behavior of the original firewall.

R. Piskac—This research was sponsored by the NSF under grants CCF-1302327, CFF-1553168, and CCF-1715387.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Agrawal, R., Imieliński, T., Swami, A.: Mining association rules between sets of items in large databases. SIGMOD Rec. 22(2), 207–216 (1993). https://doi.org/10.1145/170036.170072

  2. Cohane, R.: Financial cost of software bugs (2017). https://medium.com/@ryancohane/financial-cost-of-software-bugs-51b4d193f107

  3. Cypher, A., Halbert, D.: Watch what I Do: Programming by Demonstration. MIT Press, Cambridge (1993)

    Google Scholar 

  4. Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 229–239 (2015)

    Google Scholar 

  5. Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL, pp. 317–330 (2011)

    Google Scholar 

  6. Gulwani, S.: Synthesis from examples: interaction models and algorithms. In: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2012). Invited talk paper

    Google Scholar 

  7. Hallahan, W.T., Zhai, E., Piskac, R.: Automated repair by example for firewalls. In: 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2–6 October 2017, pp. 220–229 (2017). https://doi.org/10.23919/FMCAD.2017.8102263

  8. Lieberman, H.: Your Wish Is My Command: Programming by Example. Morgan Kaufmann, San Francisco (2001)

    Google Scholar 

  9. Menon, A.K., Tamuz, O., Gulwani, S., Lampson, B.W., Kalai, A.: A machine learning framework for programming by example. In: ICML (1), pp. 187–195 (2013)

    Google Scholar 

  10. Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 619–630 (2015)

    Google Scholar 

  11. Ryall, J.: Facebook, Tinder, Instagram suffer widespread issues (2015). http://mashable.com/2015/01/27/facebook-tinder-instagram-issues/

  12. Santolucito, M., Zhai, E., Dhodapkar, R., Shim, A., Piskac, R.: Synthesizing configuration file specifications with association rule learning. PACMPL 1(OOPSLA), 64:1–64:20 (2017). https://doi.org/10.1145/3133888

  13. Santolucito, M., Zhai, E., Piskac, R.: Probabilistic automated language learning for configuration files. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 80–87. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_5

    Chapter  Google Scholar 

  14. Singh, R., Gulwani, S.: Learning semantic string transformations from examples. PVLDB 5, 740–751 (2012)

    Google Scholar 

  15. Singh, R., Gulwani, S.: Synthesizing number transformations from input-output examples. In: CAV, pp. 634–651 (2012)

    Google Scholar 

  16. Flash Fill (Microsoft Excel 2013 feature). http://research.microsoft.com/users/sumitg/flashfill.html

  17. Xu, T., Jin, L., Fan, X., Zhou, Y., Pasupathy, S., Talwadker, R.: Hey, you have given me too many knobs!: understanding and dealing with over-designed configuration in system software. In: The 10th ESEC/FSEJoint Meeting on Foundations of Software Engineering, August 2015

    Google Scholar 

  18. Xu, T., Zhang, J., Huang, P., Zheng, J., Sheng, T., Yuan, D., Zhou, Y., Pasupathy, S.: Do not blame users for misconfigurations. In: The 24th SOSPACM Symposium on Operating Systems Principles, November 2013

    Google Scholar 

  19. Yin, Z., Ma, X., Zheng, J., Zhou, Y., Bairavasundaram, L.N., Pasupathy, S.: An empirical study on configuration errors in commercial and open source systems. In: Proceedings of the Twenty-Third ACM Symposium on Operating Systems Principles, pp. 159–172, SOSP 2011. ACM, New York (2011). https://doi.org/10.1145/2043556.2043572

Download references

Author information

Authors and Affiliations

  1. Yale University, New Haven, USA

    Ruzica Piskac

Authors
  1. Ruzica Piskac
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ruzica Piskac .

Editor information

Editors and Affiliations

  1. Universität Freiburg, Freiburg, Germany

    Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Piskac, R. (2018). New Applications of Software Synthesis: Verification of Configuration Files and Firewall Repair. In: Podelski, A. (eds) Static Analysis. SAS 2018. Lecture Notes in Computer Science(), vol 11002. Springer, Cham. https://doi.org/10.1007/978-3-319-99725-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99725-4_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99724-7

  • Online ISBN: 978-3-319-99725-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation