Abstract
Alloy is a lightweight specification language based on relational logic, with an analysis engine that relies on SAT solvers to automate bounded verification of specifications. In spite of its strengths, the reliance of the Alloy Analyzer on computationally heavy solvers means that it can take a significant amount of time to verify software properties, even within limited bounds. This challenge is exacerbated by the ever-evolving nature of complex software systems. This paper presents Platinum, a technique for efficient analysis of evolving Alloy specifications, that recognizes opportunities for constraint reduction and reuse of previously identified constraint solutions. The insight behind Platinum is that formula constraints recur often during the analysis of a single specification and across its revisions, and constraint solutions can be reused over sequences of analyses performed on evolving specifications. Our empirical results show that Platinum substantially reduces (by 66.4% on average) the analysis time required on specifications extracted from real-world software systems.
Chapter PDF
Similar content being viewed by others
References
Covert analysis tool. http://www.sdalab.com/projects/covert (2017)
Google play market. http://play.google.com/store/apps/ (2017)
WordPress. http://codex.wordpress.org/Database_Description/3.3 (2017)
Green solver. https://github.com/green-solver/green-solver/tree/master/green/test/za/ac/sun/cs/green/misc (2018)
Platinum repository. https://sites.google.com/view/platinum-repository (2019)
Aquino, A., Bianchi, F.A., Chen, M., Denaro, G., Pezzè, M.: Reusing constraint proofs in program analysis. In: Proceedings of the International Symposium on Software Testing and Analysis. pp. 305–315 (2015)
Aquino, A., Denaro, G., Pezzè, M.: Heuristically Matching Solution Spaces of Arithmetic Formulas to Efficiently Reuse Solutions. In: Proceedings of the 39th International Conference on Software Engineering. pp. 427–437. ICSE ’17, IEEE Press, Piscataway, NJ, USA (2017), https://doi.org/10.1109/ICSE.2017.46
Bagheri, H., Kang, E., Malek, S., Jackson, D.: Detection of design flaws in the android permission protocol through bounded verification. In: Bjørner, N., de Boer, F.S. (eds.) FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9109, pp. 73–89. Springer (2015), https://doi.org/10.1007/978-3-319-19249-9_6
Bagheri, H., Kang, E., Malek, S., Jackson, D.: A formal approach for detection of security flaws in the android permission system. Formal Asp. Comput. 30(5), 525–544 (2018), https://doi.org/10.1007/s00165-017-0445-z
Bagheri, H., Malek, S.: Titanium: Efficient analysis of evolving alloy specifications. In: Proceedings of the International Symposium on the Foundations of Software Engineering (2016)
Bagheri, H., Sadeghi, A., Behrouz, R.J., Malek, S.: Practical, formal synthesis and automatic enforcement of security policies for android. In: 46th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2016, Toulouse, France, June 28 - July 1, 2016. pp. 514–525. IEEE Computer Society (2016), https://doi.org/10.1109/DSN.2016.53
Bagheri, H., Sadeghi, A., Garcia, J., Malek, S.: Covert: Compositional analysis of android inter-app permission leakage. IEEE Transactions on Software Engineering (2015)
Bagheri, H., Sullivan, K.J.: Model-driven synthesis of formally precise, stylized software architectures. Formal Asp. Comput. 28(3), 441–467 (2016), https://doi.org/10.1007/s00165-016-0360-8
Bagheri, H., Tang, C., Sullivan, K.: Trademaker: Automated dynamic analysis of synthesized tradespaces. In: Proceedings of the 36th International Conference on Software Engineering. pp. 106–116. ICSE 2014, ACM, New York, NY, USA (2014), http://doi.acm.org/10.1145/2568225.2568291
Bagheri, H., Tang, C., Sullivan, K.: Automated synthesis and dynamic analysis of tradeoff spaces for object-relational mapping. IEEE Transactions on Software Engineering 43(2), 145–163 (2017)
Bagheri, H., Wang, J., Aerts, J., Malek, S.: Efficient, evolutionary security analysis of interacting android apps. In: 2018 IEEE International Conference on Software Maintenance and Evolution, ICSME 2018, Madrid, Spain, September 23-29, 2018. pp. 357–368. IEEE Computer Society (2018), https://doi.org/10.1109/ICSME.2018.00044
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, Third Edition. The MIT Press, 3rd edn. (2009)
Cunha, A., Macedo, N., Guimaraes, T.: Target oriented relational model finding. In: Proceedings of the International Conference on Fundamental Approaches to Software Engineering. pp. 17–31 (2014)
De Ita Luna, G., Marcial-Romero, J.R., Hernandez, J.: The Incremental Satisfiability Problem for a Two Conjunctive Normal Form. Electronic Notes in Theoretical Computer Science 328, 31–45 (Dec 2016), http://www.sciencedirect.com/science/article/pii/S1571066116301013
Devdatta Akhawe, Adam Barth, Peifung E. Lamy, John Mitchelly, Dawn Song: Towards a Formal Foundation of Web Security. In: Proceedings of the 23rd International Conference on Computer Security Foundations Symposium (CSF). pp. 290–304 (2010)
Een, N., Sorensson, N.: Translating pseudo-boolean constraints into sat. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006)
Egly, U., Lonsing, F., Oetsch, J.: Automated Benchmarking of Incremental SAT and QBF Solvers. In: Logic for Programming, Artificial Intelligence, and Reasoning. pp. 178–186. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (Nov 2015)
Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Proceedings of International Symposium on Software Testing and Analysis. pp. 25–36 (2010)
Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Transactions on Software Engineering 39(9), 1283–1307 (2013)
Ganov, S., Khurshid, S., Perry, D.E.: Annotations for alloy: Automated incremental analysis using domain specific solvers. In: Proc. of ICFEM. pp. 414–429 (2012)
Hao, J., Kang, E., Sun, J., Jackson, D.: Designing Minimal Effective Normative Systems with the Help of Lightweight Formal Methods. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. pp. 50–60. FSE 2016, ACM, New York, NY, USA (2016), http://doi.acm.org/10.1145/2950290.2950307
Heaven, W., Russo, A.: Enhancing the alloy analyzer with patterns of analysis. In: Workshop on Logic-based Methods in Programming Environments (2005)
Jackson, D.: Software Abstractions. MIT Press, 2nd edn. (2012)
Jia, X., Ghezzi, C., Ying, S.: Enhancing reuse of constraint solutions to improve symbolic execution. In: Proceedings of the International Symposium on Software Testing and Analysis. pp. 177–187 (2015)
Lau, S.Q.: Domain Analysis of E-Commerce Systems Using Feature-Based Model Templates. Master’s thesis, University of Waterloo, Canada (2006)
Li, X., Shannon, D., Walker, J., Khurshid, S., Marinov, D.: Analyzing the Uses of a Software Modeling Tool. Electronic Notes in Theoretical Computer Science 164(2), 3–18 (Oct 2006). https://doi.org/10.1016/j.entcs.2006.10.001, http://www.sciencedirect.com/science/article/pii/S1571066106004786
Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. pp. 373–383. FSE 2016, ACM, New York, NY, USA (2016), http://doi.acm.org/10.1145/2950290.2950318
Macedo, N., Cunha, A., Guimaraes, T.: Exploring scenario exploration. In: Proceedings of the International Conference on Fundamental Approaches to Software Engineering. pp. 301–315 (2015)
Maldonado-Lopez, F.A., Chavarriaga, J., Donoso, Y.: Detecting Network Policy Conflicts Using Alloy. In: Abstract State Machines, Alloy, B, TLA, VDM, and Z. pp. 314–317. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (Jun 2014)
Mansoor, N., Saddler, J.A., Silva, B., Bagheri, H., Cohen, M.B., Farritor, S.: Modeling and testing a family of surgical robots: an experience report. In: Leavens, G.T., Garcia, A., Pasareanu, C.S. (eds.) Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, November 04-09, 2018. pp. 785–790. ACM (2018), https://doi.org/10.1145/3236024.3275534
Marinov, D., Khurshid, S.: What will the user do (next) in the tool? In: Proceedings of the ACM SIGSOFT First Alloy Workshop. pp. 98–99. ACM (2006)
Milicevic, A., Rayside, D., Yessenov, K., Jackson, D.: Unifying execution of imperative and declarative code. In: Proceedings of the 33rd International Conference on Software Engineering. pp. 511–520. ICSE ’11, ACM, New York, NY, USA (2011), http://doi.acm.org/10.1145/1985793.1985863
Mirzaei, N., Garcia, J., Bagheri, H., Sadeghi, A., Malek, S.: Reducing combinatorics in GUI testing of android applications. In: Dillon, L.K., Visser, W., Williams, L. (eds.) Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016. pp. 559–570. ACM (2016), https://doi.org/10.1145/2884781.2884853
Montaghami, V., Rayside, D.: Extending Alloy with partial instances. In: Proceedings of the International Conferece on Abstract State Machines, Alloy, B, VDM, and Z. pp. 122–135 (2012)
Montaghami, V., Rayside, D.: Staged evaluation of partial instances in a relational model finder. In: Proceedings of the International Conferece on Abstract State Machines, Alloy, B, VDM, and Z. pp. 318–323 (2014)
Montaghami, V., Rayside, D.: Bordeaux: A tool for thinking outside the box. In: Proceedings of the International Conference on Fundamental Approaches to Software Engineering. pp. 22–39 (2017)
Nadel, A., Ryvchin, V., Strichman, O.: Ultimately Incremental SAT. In: Theory and Applications of Satisfiability Testing (SAT 2014). pp. 206–218. Lecture Notes in Computer Science, Springer, Cham (Jul 2014)
Near, J.P., Jackson, D.: Derailer: Interactive security analysis for web applications. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering. pp. 587–598. ASE ’14, ACM, New York, NY, USA (2014), http://doi.acm.org/10.1145/2642937.2643012
Nelson, T., Danas, N., Dougherty, D.J., Krishnamurthi, S.: The Power of "Why" and "Why Not": Enriching Scenario Exploration with Provenance. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering. pp. 106–116. ESEC/FSE 2017, ACM, New York, NY, USA (2017), http://doi.acm.org/10.1145/3106237.3106272
Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: Principled scenario exploration through minimality. In: Proceedings of the International Conference on Software Engineering. pp. 232–241 (2013)
Nijjar, J., Bultan, T.: Bounded verification of ruby on rails data models. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis. pp. 67–77. ISSTA ’11, ACM, New York, NY, USA (2011), http://doi.acm.org/10.1145/2001420.2001429
Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: Proceedings of the Conference on Programming Language Design and Implementation. pp. 504–515 (2011)
Ponzio, P., Aguirre, N., Frias, M.F., Visser, W.: Field-exhaustive Testing. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. pp. 908–919. FSE 2016, ACM, New York, NY, USA (2016), http://doi.acm.org/10.1145/2950290.2950336
Qiu, R., Yang, G., Pasareanu, C.S., Khurshid, S.: Compositional symbolic execution with memoized replay. In: Proceedings of the International Conference on Software Engineering (2015)
Ramos, D.A., Engler, D.R.: Practical, low-effort equivalence verification of real code. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification, Lecture Notes in Computer Science, vol. 6806, pp. 669–685. Springer Berlin Heidelberg (2011), http://dx.doi.org/10.1007/978-3-642-22110-1_55
Rosner, N., Siddiqui, J.H., Aguirre, N., Khurshid, S., Frias, M.F.: Ranger: Parallel analysis of Alloy models by range partitioning. In: Proceeding of the International Conference on Automated Software Engineering. pp. 147–157 (2013)
Ruchansky, N., Proserpio, D.: A (Not) NICE Way to Verify the Openflow Switch Specification: Formal Modelling of the Openflow Switch Using Alloy. In: Proceedings of the ACM SIGCOMM 2013 Conference on SIGCOMM. pp. 527–528. SIGCOMM ’13, ACM, New York, NY, USA (2013), http://doi.acm.org/10.1145/2486001.2491711
Semerath, O., Varas, A., Varra, D.: Iterative and Incremental Model Generation by Logic Solvers. In: Fundamental Approaches to Software Engineering. pp. 87–103. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (Apr 2016), https://link.springer.com/chapter/10.1007/978-3-662-49665-7_6
Stevens, C., Bagheri, H.: Reducing run-time adaptation space via analysis of possible utility bounds. In: Proceedings of the 42nd International Conference on Software Engineering. ICSE 2020, ACM (2020)
Taghdiri, M.: Inferring specifications to detect errors in code. In: Proceedings of the 19th IEEE International Conference on Automated Software Engineering. pp. 144–153. ASE ’04, IEEE Computer Society, Washington, DC, USA (2004), http://dx.doi.org/10.1109/ASE.2004.42
Torlak, E.: A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications. PhD thesis, MIT (Feb 2009), http://alloy.mit.edu/kodkod/
Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 632–647. TACAS’07, Springer-Verlag, Berlin, Heidelberg (2007), http://dl.acm.org/citation.cfm?id=1763507.1763571
Torlak, E., Taghdiri, M., Dennis, G., Near, J.P.: Applications and extensions of Alloy: Past, present and future. Mathematical Structures in Computer Science 23(4), 915–933 (2013)
Uzuncaova, E., Khurshid, S.: Kato: A program slicing tool for declarative specifications. In: Proceedings of the International Conference on Software Engineering. pp. 767–770 (2007)
Uzuncaova, E., Khurshid, S.: Constraint prioritization for efficient analysis of declarative models. In: Proceedings of the International Symposium on Formal Methods (2008)
Uzuncaova, E., Khurshid, S., Batory, D.: Incremental test generation for software product lines. IEEE Trans. Software Eng. 36(3), 309–322 (2010)
Visser, W., Geldenhuys, J., , Dwyer, M.B.: Green: Reducing, reusing and recycling constraints in program analysis. In: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering. pp. 58:1–58:11 (2012)
Wang, J., Bagheri, H., Cohen, M.B.: An evolutionary approach for analyzing alloy specifications. In: Huchard, M., Kästner, C., Fraser, G. (eds.) Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018. pp. 820–825. ACM (2018), https://doi.org/10.1145/3238147.3240468
Wang, K.: MuAlloy: an automated mutation system for alloy. Thesis (May 2015), https://repositories.lib.utexas.edu/handle/2152/31865
Yang, G., Păsăreanu, C.S., Khurshid, S.: Memoized symbolic execution. In: Proceedings of the International Symposium on Software Testing and Analysis. pp. 144–154 (2012)
Zave, P.: Using Lightweight Modeling to Understand Chord. SIGCOMM Comput. Commun. Rev. 42(2), 49–57 (Mar 2012), http://doi.acm.org/10.1145/2185376.2185383
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Zheng, G., Bagheri, H., Rothermel, G., Wang, J. (2020). Platinum: Reusing Constraint Solutions in Bounded Analysis of Relational Logic. In: Wehrheim, H., Cabot, J. (eds) Fundamental Approaches to Software Engineering. FASE 2020. Lecture Notes in Computer Science(), vol 12076. Springer, Cham. https://doi.org/10.1007/978-3-030-45234-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-45234-6_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45233-9
Online ISBN: 978-3-030-45234-6
eBook Packages: Computer ScienceComputer Science (R0)