Hostname: page-component-586b7cd67f-gb8f7 Total loading time: 0 Render date: 2024-11-25T19:40:28.221Z Has data issue: false hasContentIssue false
  • English
  • Français

Making abstract models complete†

Published online by Cambridge University Press:  12 November 2014

ROBERTO GIACOBAZZI  and
ISABELLA MASTROENI
ROBERTO GIACOBAZZI
Affiliation:
Universitá degli Studi di Verona, Dipartimento di Informatica Strada Le Grazie, 15, 37134 Verona, Italy Email: [email protected] and [email protected]
ISABELLA MASTROENI
Affiliation:
Universitá degli Studi di Verona, Dipartimento di Informatica Strada Le Grazie, 15, 37134 Verona, Italy Email: [email protected] and [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Completeness is a key feature of abstract interpretation. It corresponds to exactness of the abstraction of fix-points and relies upon the need of absence of false alarms in static program analysis. Making abstract interpretation complete is therefore a major problem in approximating the semantics of programming languages. In this paper, we consider the problem of making abstract interpretations complete by minimally modifying the predicate transformer, i.e. the semantics, of a program. We study the mathematical properties of complete functions on complete lattices and prove the existence of minimal transformations of monotone functions to achieve completeness. We then apply minimal complete transformers to prove the minimality of standard program transformations in security, such as static program monitoring.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Issue 4 , May 2016 , pp. 658 - 701
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

This is a revised and extended version of two papers that appeared in the Proceedings of SAS'08 (Giacobazzi and Mastroeni 2008) and SEFM'08 (Giacobazzi 2008).

References

Abramsky, S. and Jung, A. (1994) Domain theory. In: Abramsky, S., Gabbay, D. M. and Maibaum, T. S. E. (eds.) Handbook of Logic in Computer Science, volume 3, Oxford University Press, Inc. 1–168.Google Scholar
Ball, T., Podelski, A. and Rajamani, S. (2002) Relative completeness of abstraction refinement for software model checking. In: Kaoen, J.-P. and Stevens, P. (eds.) Proceedings of TACAS: Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag Lecture Notes in Computer Science 2280 158–172.Google Scholar
Blyth, T. and Janowitz, M. (1972) Residuation Theory, Pergamon Press.Google Scholar
Clarke, E. M., Grumberg, O., Jha, S., Lu, Y. and Veith, H. (2003) Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50 (5) 752–794.Google Scholar
Collberg, C. and Nagra, J. (2010) Surreptitious Software, Addison Wesley.Google Scholar
Collberg, C. and Thomborson, C. D. (1999) Software watermarking: Models and dynamic embeddings. In: POPL'99: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, New York, NY, USA 311–324.Google Scholar
Collberg, C. and Thomborson, C. D. (2000) Watermarking, tamper-proofing, and obfuscation-tools for software protection. IEEE Transactions on Software Engineering 28 735–746.Google Scholar
Cousot, P. (2002) Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science 277 (1–2) 47–103.Google Scholar
Cousot, P. and Cousot, R. (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fix-points. In: Proceedings of Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL'77), ACM Press, New York 238–252.Google Scholar
Cousot, P. and Cousot, R. (1979a) A constructive characterization of the lattices of all retractions, preclosure, quasi-closure and closure operators on a complete lattice. Portuguese Mathematical 38 (2) 185–198.Google Scholar
Cousot, P. and Cousot, R. (1979b) Constructive versions of Tarski's fixed point theorems. Pacific Journal of Mathematics 82 (1) 43–57.Google Scholar
Cousot, P. and Cousot, R. (1979c) Systematic design of program analysis frameworks. In: Proceedings of Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL'79), ACM Press, New York 269–282.Google Scholar
Cousot, P. and Cousot, R. (1992a) Abstract interpretation frameworks. Journal of Logic and Computation 2 (4) 511–547.Google Scholar
Cousot, P. and Cousot, R. (1992b) Comparing the Galois connection and widening/narrowing approaches to abstract interpretation (Invited Paper) In: Bruynooghe, M. and Wirsing, M. (eds.) Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming (PLILP'92). Springer-Verlag Lecture Notes in Computer Science 631 269–295.Google Scholar
Cousot, P. and Cousot, R. (2002) Systematic design of program transformation frameworks by abstract interpretation. In: Proceedings of Conference Record of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York 178–190.Google Scholar
Cousot, P. and Cousot, R. (2004) An abstract interpretation-based framework for software watermarking. In: Conference Record of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Venice, Italy. ACM Press 173–185.Google Scholar
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min, A., Monniaux, D. and Rival, X. (2007a) Combination of abstractions in the Astrée static analyzer. In: Okada, M. and Satoh, I. (eds.) 11th Annual Asian Computing Science Conference (ASIAN'06). Springer Lecture Notes in Computer Science 4435 1–24.Google Scholar
Cousot, P., Ganty, P. and Raskin, J.-F. (2007b) Fixpoint-guided abstraction refinements. In: Filé, G. and Riis Nielson, H. (eds.) Proceedings of the 14th International Symposium on Static Analysis, SAS '07, Kongens Lyngby, Denmark. Springer Lecture Notes in Computer Science 4634 333–348.Google Scholar
Dalla Preda, M., Christodorescu, M., Jha, S. and Debray, S. (2007) A semantics-based approach to malware detection. In: POPL'07: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, NY, USA 377–388.Google Scholar
Dalla Preda, M. and Giacobazzi, R. (2009) Semantic-based code obfuscation by abstract interpretation. Journal of Computer Security 17 (6) 855–908.Google Scholar
Dams, D., Gerth, R. and Grumberg, O. (1997) Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems 19 (2) 253–291.Google Scholar
Davey, B. A. and Priestley, H. A. (1990) Introduction to Lattices and Order, Cambridge University Press, Cambridge, U.K. Google Scholar
Erlingsson, U. and Schneider, F. (1999) Sasi enforcement of security policies: A retrospective. In: NSPW'99, ACM Press, New York 87–95.Google Scholar
Filé, G., Giacobazzi, R. and Ranzato, F. (1996) A unifying view of abstract domain design. ACM Computing Surveys 28 (2) 333–336.CrossRefGoogle Scholar
Giacobazzi, R. (2008) Hiding information in completeness holes – new perspectives in code obfuscation and watermarking. In: Proceedings of The 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), IEEE Press 7–20.Google Scholar
Giacobazzi, R., Jones, N. and Mastroeni, I. (2012) Obfuscation by partial evaluation of distorted interpreters. In: Proceedings of the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM'12), ACM Press, New York 179–185.Google Scholar
Giacobazzi, R. and Mastroeni, I. (2004) Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: Proceedings of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '04), ACM-Press, New York 186–197.Google Scholar
Giacobazzi, R. and Mastroeni, I. (2008) Transforming abstract interpretations by abstract interpretation. In: Alpuente, M. (ed.) Proceedings of the 15th International Static Analysis Symposium, SAS'08. Springer-Verlag Lecture Notes in Computer Science 5079 1–17.Google Scholar
Giacobazzi, R. and Quintarelli, E. (2001) Incompleteness, counterexamples and refinements in abstract model-checking. In: Cousot, P. (ed.) Proceedings of The 8th International Static Analysis Symposium (SAS'01). Springer-Verlag Lecture Notes in Computer Science 2126 356–373.Google Scholar
Giacobazzi, R. and Ranzato, F. (1997) Refining and compressing abstract domains. In: Degano, P., Gorrieri, R. and Marchetti-Spaccamela, A. (eds.) Proceedings of the 24th International Colloquium on Automata, Languages and Programming (ICALP '97). Springer-Verlag Lecture Notes in Computer Science 1256 771–781.Google Scholar
Giacobazzi, R. and Ranzato, F. (1998a) Optimal domains for disjunctive abstract interpretation. Science of Computer Programming 32 (1–3) 177–210.Google Scholar
Giacobazzi, R. and Ranzato, F. (1998b) Uniform closures: Order-theoretically reconstructing logic program semantics and abstract domain refinements. Information and Computation 145 (2) 153–190.CrossRefGoogle Scholar
Giacobazzi, R., Ranzato, F. and Scozzari, F. (2000) Making abstract interpretations complete. Journal of the ACM 47 (2) 361–416.Google Scholar
Gulavani, B. S. and Rajamani, S. K. (2006) Counterexample driven refinement for abstract interpretation. In: TACAS 06: Tools and Algorithms for Construction and Analysis of Systems. Springer Lecture Notes in Computer Science 3920 474–488.Google Scholar
Gumm, H. P. (1993) Another glance at the Alpern–Schneider theorem. Information Processing Letters 47 291–294.Google Scholar
Janowitz, M. F. (1967) Residuated closure operators. Portuguese Mathematical 26 (2) 221–252.Google Scholar
Kihara, M., Fujiyoshi, M., Wan, Q. T. and Kiya, H. (2007) Image tamper detection using mathematical morphology. In: ICIP 2007: IEEE International Conference on Image Processing, IEEE 101–104.Google Scholar
Laviron, V. and Logozzo, F. (2009) Refining abstract interpretation-based static analyses with hints. In: Proceedings of APLAS'09. Springer-Verlag Lecture Notes in Computer Science 5904 343–358.Google Scholar
Mastroeni, I. (2004) Algebraic power analysis by abstract interpretation. Higher-Order and Symbolic Computation (HOSC) 17 (4) 299–347.Google Scholar
Mastroeni, I. (2008) Deriving bisimulations by simplifying partitions. In: Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'08). Springer-Verlag Lecture Notes in Computer Science 4905 147–171.Google Scholar
Mastroeni, I. and Giacobazzi, R. (2011) An abstract interpretation-based model for safety semantics. Journal of Computer Mathematics 88 (4) 665–694.Google Scholar
Mycroft, A. (1993) Completeness and predicate-based abstract interpretation. In: Proceedings of the ACM Symposium on Partial Evaluation and Program Manipulation (PEPM'93), ACM Press, New York 179–185.Google Scholar
Nagra, J. and Thomborson, C. D. (2004) Threading software watermarks. In: Proceedings of 6th International Workshop on Information Hiding. Springer-Verlag Lecture Notes in Computer Science 3200 208–233.CrossRefGoogle Scholar
Nagra, J., Thomborson, C. D. and Collberg, C. (2002) A functional taxonomy for software watermarking. Australian Computer Science Communications 24 (1) 177–186.Google Scholar
Nielson, F., Nielson, H. and Hankin, C. (1999) Principles of Program Analysis, Springer.Google Scholar
Ranzato, F. and Tapparo, F. (2007) Generalized strong preservation by abstract interpretation. Journal of Logic and Computation 17 (1) 157–197.Google Scholar
Rival, X. and Mauborgne, L. (2007) The trace partitioning abstract domain. ACM Transactions on Programming Languages and Systems 29 (5) 26.Google Scholar
Schneider, F. B. (2000) Enforceable security policies. Information and System Security 3 (1) 30–50.Google Scholar
Vechev, M. T., Yahav, E. and Yorsh, G. (2010) Abstraction-guided synthesis of synchronization. In: Proceedings of the 37th ACM SIGPLAN-SIGACT POPL 2010, ACM 327–338.Google Scholar
Venkatesan, R., Vazirani, V. and Sinha, S. (2001) A graph theoretic approach to software watermarking. In: Information Hiding. Lecture Notes in Computer Science 2137 157–168.Google Scholar
Ward, M. (1942) The closure operators of a lattice. Annals of Mathematical 43 (2) 191–196.Google Scholar