Abstract
Yuri Gurevich and Itay Neeman proposed the Distributed Knowledge Authorization Language, DKAL, as an expressive, yet very succinct logic for distributed authorization. DKAL uses a combination of modal and intuitionistic propositional logic. Modalities are used for qualifying assertions made by different principals and intuitionistic logic captures very elegantly assertions about basic information. Furthermore, a non-trivial and useful fragment known as the primal infon logic is amenable to efficient linear-time saturation.
In this paper we experiment with an embedding of the full DKAL logic into the state-of-the-art Satisfiability Modulo Theories solver Z3 co-developed by the second author. Z3 supports classical first-order semantics of formulas, so it is not possible to directly embed DKAL into Z3. We therefore use an indirect encoding. The one experimented with in this paper uses the instantiation-based support for quantifiers in Z3.
Z3 offers the feature to return a potential ground counter-model when the saturation procedure ends up with a satisfiable set of ground assertions. We develop an algorithm that extracts a DKAL model from the propositional model, in order to provide root causes for non-derivability.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. SIGPLAN Not. 37(1), 1–3 (2002)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Bjørner, N., Hendrix, J.: Linear functional fixed-points. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 124–139. Springer, Heidelberg (2009)
Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A Precise Yet Efficient Memory Model For C. In: Proceedings of Systems Software Verification Workshop (SSV 2009) (2009) (to appear)
Costa, M., Crowcroft, J., Castro, M., Rowstron, A.I.T., Zhou, L., Zhang, L., Barham, P.: Vigilante: end-to-end containment of internet worms. In: Herbert, A., Birman, K.P. (eds.) SOSP, pp. 133–147. ACM, New York (2005)
de Moura, L., Bjørner, N.: Efficient E-Matching for SMT Solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Degtyarev, A., Gurevich, Y., Narendran, P., Veanes, M., Voronkov, A.: Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Theoretical Computer Science 243, 167–184 (2000)
DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report 2005-70, Microsoft Research (2005)
Godefroid, P., Levin, M., Molnar, D.: Automated Whitebox Fuzz Testing. Technical Report 2007-58, Microsoft Research (2007)
Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: a new algorithm for property checking. In: Young, M., Devanbu, P.T. (eds.) SIGSOFT FSE, pp. 117–127. ACM, New York (2006)
Gurevich, Y., Neeman, I.: Dkal: Distributed-knowledge authorization language. In: CSF, pp. 149–162. IEEE Computer Society, Los Alamitos (2008)
Gurevich, Y., Neeman, I.: DKAL 2 — A Simplified and Improved Authorization Language. Technical Report 2009-11, Microsoft Research (2009)
Gurevich, Y., Neeman, I.: The Infon Logic. Bulletin of European Association for Theoretical Computer Science (2009)
Jackson, E.K., Schulte, W.: Model Generation for Horn Logic with Stratified Negation. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 1–20. Springer, Heidelberg (2008)
Lahiri, S.K., Qadeer, S.: Back to the Future: Revisiting Precise Program Verification using SMT Solvers. In: POPL 2008 (2008)
Mints, G.: Grigori. In: A short introduction to intuitionistic logic. Kluwer Academic, New York (2000)
Moy, Y., Bjørner, N., Sielaff, D.: Modular Bug-finding for Integer Overflows in the Large: Sound, Efficient, Bit-precise Static Analysis. Technical Report MSR-TR-2009-57, Microsoft Research (2009)
Ohlbach, H.J., Nonnengart, A., de Rijke, M., Gabbay, D.M.: Encoding two-valued nonclassical logics in classical logic. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1403–1486. Elsevier, MIT Press (2001)
Tillmann, N., Schulte, W.: Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution. IEEE software 23, 38–47 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Mera, S., Bjørner, N. (2010). DKAL and Z3: A Logic Embedding Experiment. In: Blass, A., Dershowitz, N., Reisig, W. (eds) Fields of Logic and Computation. Lecture Notes in Computer Science, vol 6300. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15025-8_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-15025-8_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15024-1
Online ISBN: 978-3-642-15025-8
eBook Packages: Computer ScienceComputer Science (R0)