Modular verification of programs with effects and effects handlers. (English) Zbl 1458.68119

Summary: Modern computing systems have grown in complexity, and even though system components are generally carefully designed and even verified by different groups of people, the composition of these components is often regarded with less attention. Inconsistencies between components’ assumptions on the rest of the system can have significant repercussions on this system, and may ultimately lead to safety or security issues. In this article, we introduce FreeSpec, a formalism built upon the key idea that components can be modeled as programs with algebraic effects to be realized by other components. FreeSpec allows for the modular modeling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition. In addition, we have implemented a framework for the Coq proof assistant based on FreeSpec.


68Q60 Specification and verification (program logics, model checking, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI


[1] Abel A, Benke M, Bove A, Hughes J, Norell U (2005) Verifying Haskell programs using constructive type theory. In: Leijen D (ed) Proceedings of the ACM SIGPLAN workshop on Haskell, Haskell 2005, Tallinn, Estonia, September 30, 2005. ACM, pp 62-73
[2] Abrial, J-R, The B-book: assigning programs to meanings (2005), Cambridge: Cambridge University Press, Cambridge
[3] Apfelmus H (2010) The operational package. https://hackage.haskell.org/package/operational
[4] Bélanger OS, Appel AW (2017) Shrink fast correctly! In: Vanhoof W, Pientka B (eds) Proceedings of the 19th international symposium on principles and practice of declarative programming, Namur, Belgium, October 09-11, 2017. ACM, pp 49-60
[5] Barnett, M.; Fähndrich, M.; Rustan, K.; Leino, M.; Müller, P.; Schulte, W.; Venter, H., Specification and verification: the spec# experience, Commun ACM, 54, 6, 81-91 (2011)
[6] Bauer, A.; Pretnar, M., Programming with algebraic effects and handlers, J Logic Algeb Methods Program, 84, 1, 108-123 (2015) · Zbl 1304.68025
[7] Thomas, Braibant, Coquet: a Coq library for verifying hardware, CPP, 7086, 330-345 (2011) · Zbl 1350.68226
[8] Brady E (2014) Resource-dependent algebraic effects. In: international symposium on trends in functional programming. Springer, Berlin, vol 8843, pp 18-33
[9] Claret G, Yann R-G (2015) Mechanical verification of interactive programs specified by use cases. In: Proceedings of the third FME workshop on formal methods in software engineering. IEEE Press, pp 61-67
[10] Choi J,Vijayaraghavan M, Sherman B, Chlipala A et al (2017) Kami: a platform for high-level parametric hardware specification and its modular verification. In: Proceedings of the ACM on programming languages, 1(ICFP):24
[11] Dylus, S.; Christiansen, J.; Teegen, F., One Monad to prove them all, Program J, 3, 3, 8 (2019)
[12] DeepSpec. DeepSpec: The Science of Deep Specification
[13] Duflot, L.; Levillain, O.; Morin, B.; Grumelard, O., Getting into the SMRAM: SMM reloaded (2009), Vancouver, Canada: CanSecWest, Vancouver, Canada
[14] Flanagan, C.; Rustan, K.; Leino, M.; Lillibridge, M.; Nelson, G.; Saxe, JB; Stata, R., PLDI 2002: extended static checking for Java, SIGPLAN Not, 48, 4, 22-33 (2013)
[15] Hur C-K, Georg N, Derek D, Viktor V (2013) The power of parameterization in coinductive proof. In: Giacobazzi R, Cousot R (eds) The 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’13, Rome, Italy—January 23-25, 2013. ACM, pp 193-206 · Zbl 1301.68220
[16] Heyman T, Scandariato R, Joosen W (2012) Reusable formal models for secure software architectures. In: 2012 joint working IEEE/IFIP conference on software architecture and european conference on software architecture, WICSA/ECSA 2012, Helsinki, Finland, August 20-24, 2012, pp 41-50
[17] Hinze R, Voigtländer J(eds) (2015) Mathematics of program construction—12th international conference, MPC 2015, Königswinter, Germany, June 29-July 1, 2015. Proceedings, volume 9129 of Lecture notes in computer science. Springer, Berlin · Zbl 1312.68008
[18] Inria. The Coq Proof Assistant. https://coq.inria.fr/
[19] Jackson, D., Software abstractions: logic, language and analysis (2012), Cambridge: MIT Press, Cambridge
[20] Jomaa N, Nowak D, Grimaud G, Hym S (2016) Formal proof of dynamic memory isolation based on MMU. In: 2016 10th international symposium on theoretical aspects of software engineering (TASE). IEEE, pp 73-80
[21] Kiselyov, O.; Ishii, H., Freer monads, more extensible effects, ACM SIGPLAN notices. ACM, 50, 94-105 (2015)
[22] Koh N, Li Y, Li Y, Xia L, Beringer L, Honoré W, Mansky W, Pierce BC, Zdancewic S (2019) From C to interaction trees: specifying, verifying, and testing a networked server. In: Mahboubi A, Myreen MO (eds) Proceedings of the 8th ACM SIGPLAN international conference on certified programs and proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019 ACM, pp 234-248
[23] Letan T, Chifflier P, Hiet G, Néron P, Morin B (2016) SpecCert: specifying and verifying hardware-based security enforcement. In: 21st international symposium on formal methods (FM 2016). Springer, Berlin, vol 9995
[24] Letan T (2018) FreeSpec: a compositional reasoning framework for the Coq theorem prover https://github.com/lthms/speccert
[25] Liang S, Hudak P, Jones M (1995) Monadtrans formers and modular interpreters. In: Proceedings of the 22nd ACM SIGPLANSIGACT symposium on principles of programming languages. ACM, pp 333-343
[26] Letan T, Yann R-G, Pierre C, Guillaume H (2018) Modular verification of programs with effects and effects handlers in Coq. In: 22st international symposium on formal methods (FM 2018). Springer, Berlin, vol 10951
[27] Liskov, B.; Wing, JM, A behavioral notion of subtyping, ACM Trans Program Lang Syst, 16, 6, 1811-1841 (1994)
[28] Meyer, B., Applying “design by contract”, IEEE Comput, 25, 10, 40-51 (1992)
[29] Morrisett, G.; Tan, G.; Tassarotti, J.; Tristan, J-B; Gan, E., RockSalt: better, faster, stronger SFI for the x86, ACMSIGPLAN notices. ACM, 47, 395-404 (2012)
[30] Nanevski, A.; Morrisett, G.; Shinnar, A.; Govereau, P.; Birkedal, L., Y not: dependent types for imperative programs, ACM sigplan notices. ACM, 43, 229-240 (2008) · Zbl 1323.68142
[31] Odersky M, Zenger M (2005) Scalable component abstractions. In: Johnson RE, Gabriel RP (eds) Proceedings of the 20th annual ACM SIGPLAN conference on object-oriented programming, systems, languages, and applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA. ACM, pp 41-57
[32] Parnas, DL, A technique for software module specification with examples (Reprint), Commun ACM, 26, 1, 75-78 (1983)
[33] Pessaux F (2014) FoCaLiZe: inside an F-IDE. arXiv preprint arXiv:1404.6607
[34] Peyton Jones S (2001) Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. Engineering theories of software construction · Zbl 0989.68021
[35] Reynolds JC (2002) Separation logic: a logic for sharedmutable data structures. In: 17th IEEE symposium on logic in computer science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, pp 55-74
[36] Uustalu T (2017) Container combinatorics: monads and lax monoidal functors. In: Mousavi MR, Sgall J (eds) Topics in theoretical computer science—second IFIP WG 1.8 international conference, TTCS 2017, Tehran, Iran, September 12-14, 2017, Proceedings, lecture notes in computer science. Springer, Berlin, vol 10608, pp 91-105 · Zbl 1485.18004
[37] Wadler, P., Comprehending Monads. Math Struct Comput Sci, 2, 4, 461-493 (1992) · Zbl 0798.68040
[38] Wing, JM, A call to action: look beyond the horizon, IEEE Secur Privacy, 6, 62-67 (2003)
[39] Wojtczuk R, Rutkowska J (2009) Attacking SMM memory via intel CPU cache poisoning. Invisible Things Lab
[40] Xia L, Zakowski Y, He P Hur C-K, Malecha G, Pierce BC, Zdancewic S (2019) Interaction trees: representing recursive and impure programs in Coq (work in progress). CoRR arXiv:1906.00046
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.