Advertisement

ML Supported Predictions for SAT Solvers Performance

  • A. M. Leventi-PeetzEmail author
  • Jörg-Volker Peetz
  • Martina Rohde
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 1069)

Abstract

In order to classify the indeterministic termination behavior of the open source SAT solver CryptoMiniSat in multi-threading mode while processing hard to solve Boolean satisfiability problem instances, internal solver runtime parameters have been collected and analyzed. A subset of these parameters have been selected and employed as features vector to successfully create a machine learning model for the binary classification of the solver’s termination behavior with any single new solving run of a not yet solved instance. The model can be used for the early estimation of a solving attempt as belonging or not belonging to the class of candidates with good chances for a fast termination. In this context, a combination of active profiles of runtime characteristics appear to mirror the influence of the solver’s momentary heuristics on the immediate quality of the solver’s resolution process. Because runtime parameters of already the first two solving iterations are enough to forecast termination of the attempt with good success scores, the results of the present work deliver a promising basis which can be further developed in order to enrich CryptoMiniSat or generally any modern SAT solver with AI abilities.

Keywords

AI (Artificial Intelligence) ML (Machine Learning) SAT solver Security 

References

  1. 1.
    Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. Int. J. Inf. Sec. 7(1), 3–32 (2006)CrossRefGoogle Scholar
  2. 2.
    Biere, A., Fröhlich, A.: Evaluating CDCL restart schemes. In: Proceedings of the International Workshop on Pragmatics of SAT (POS 2015), 16 p. (2015). http://fmv.jku.at/papers/BiereFroehlich-POS15.pdf
  3. 3.
    Chollet, F., et al.: Keras (2015). https://keras.io
  4. 4.
    Devlin, D., O’Sullivan, B.: Satisfiability as a classification problem. In: Proceedings of the 19th Irish Conference on Artificial Intelligence and Cognitive Science (2008). http://www.cs.ucc.ie/~osullb/pubs/classification.pdf
  5. 5.
    Ganesh, V.: Machine Learning for SAT Solvers. Abstract. (2018) https://uwaterloo.ca/artificial-intelligence-institute/events/machine-learning-sat-solvers. Invited talk at Waterloo AI Institute, University of Waterloo, Canada
  6. 6.
    Hughes, G., Bultan, T.: Automated verification of access control policies using a SAT solver. Int. J. Softw. Tools Technol. Transf. 10(6), 503–520 (2008)CrossRefGoogle Scholar
  7. 7.
    Hutter, F., Xu, L., Hoos, H.H., Leyton-Brown, K.: Algorithm runtime prediction: methods & evaluation. Artif. Intell. 206, 79–111 (2014)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Järvisalo, M.: Boolean satisfiability and beyond: algorithms, analysis, and AI applications. In: Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), pp. 4066–4069. AAAI Press (2016). http://www.ijcai.org/Proceedings/16/Papers/602.pdf
  9. 9.
    Kehui, W., Tao, W., Xinjie, Z., Huiying, L.: CryptoMiniSAT solver based algebraic side-channel attack on PRESENT. In: 2011 First International Conference on Instrumentation, Measurement, Computer, Communication and Control, pp. 561–565 (2011)Google Scholar
  10. 10.
    Lafitte, F., Nakahara Jr., J., Van Heule, D.: Applications of SAT solvers in cryptanalysis: finding weak keys and preimages. J. Satisfiability Boolean Model. Comput. 9, 1–25 (2014)MathSciNetGoogle Scholar
  11. 11.
    Leventi-Peetz, A., Zendel, O., Lennartz, W., Weber, K.: CryptoMiniSat switches-optimization for solving cryptographic instances. In: Proceedings of the International Workshop on Pragmatics of SAT (POS 2018) (2018). https://easychair.org/publications/preprint/Q4kv
  12. 12.
    Liang, J.H.,  Ganesh, V.,  Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Theory and Applications of Satisfiability Testing - SAT 2016, Bordeaux, France, Proceedings, pp. 123–140 (2016)CrossRefGoogle Scholar
  13. 13.
    Liang, J.H., Oh, C., Mathews, M., Thomas, C., Li, C.,  Ganesh, V.: A machine learning based restart policy for CDCL SAT solvers. In: Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT 2018), pp. 94–110. Springer (2018)Google Scholar
  14. 14.
    Lindauer, M., Eggensperger, K., Feurer, M., Falkner, S., Biedenkapp, A., Hutter, F.: SMAC v3: algorithm configuration in python (2017). https://github.com/automl/SMAC3
  15. 15.
    Lorenz, C., Schnor, B.: Policy anomaly detection for distributed IPv6 firewalls. In: Proceedings of the 12th International Conference on Security and Cryptography (SECRYPT-2015), pp. 210–219. Science and Technology Publications (2015)Google Scholar
  16. 16.
    Mauro, J., Nieke, M., Seidl, C., Yu, I.C.: Anomaly detection and explanation in context-aware software product lines. In: Proceedings of the 21st International Systems and Software Product Line Conference, SPLC 2017, Volume B, Sevilla, Spain, pp. 18–21 (2017). https://www.isf.cs.tu-bs.de/cms/team/nieke/papers/2017-SPLC.pdf
  17. 17.
    Otpuschennikov, I.,  Semenov, A., Gribanova, I., Zaikin, O., Kochemazov, S.: Encoding Cryptographic Functions to SAT Using Transalg System. arXiv:1607.00888 (2016)
  18. 18.
    Rintanen, J.: Solving AI Planning Problems with SAT (2013). http://www.epcl-study.eu/content/downloads/slides/rintanen_2013.pdf. Research talk at the EPCL Basic Training Camp
  19. 19.
    Semenov, A.A., Zaikin, O., Otpuschennikov, I.V., Kochemazov, S., Ignatiev, A.: On cryptographic attacks using backdoors for SAT. In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), New Orleans, Louisiana, USA, 2018, pp. 6641–6648 (2018)Google Scholar
  20. 20.
    Soos, M., Nohl, K.,  Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Theory and Applications of Satisfiability Testing - SAT2009, 12th International Conference, SAT 2009, Swansea, UK, 30 June–3 July, 2009. Proceedings, pp. 244–257 (2009).https://github.com/msoos/cryptominisat
  21. 21.
    Vanhoef, M., Piessens, F.: Symbolic execution of security protocol implementations: handling cryptographic primitives. In: USENIX Workshop on Offensive Technology (USENIX WOOT) (2018). https://papers.mathyvanhoef.com/woot2018.pdf

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  • A. M. Leventi-Peetz
    • 1
    Email author
  • Jörg-Volker Peetz
    • 2
  • Martina Rohde
    • 1
  1. 1.Federal Office for Information SecurityBonnGermany
  2. 2.BonnGermany

Personalised recommendations