Multi-stage programming (MSP) is a style of writing program generators---programs which generate programs---supported by special annotations that direct construction, combination, and execution of object programs. Various researchers have shown MSP to be effective in writing efficient programs without sacrificing genericity. However, correctness proofs of such programs have so far received limited attention, and approaches and challenges for that task have been largely unexplored. In this thesis, I establish formal equational properties of the multi-stage lambda calculus and related proof techniques, as well as results that delineate the intricacies of multi-stage languages that one must be aware of. In particular, I settle three basic questions that naturally arise when verifying multi-stage functional programs. Firstly, can adding staging MSP to a language compromise the interchangeability of terms that held in the original language? Unfortunately it can, and more care is needed to reason about terms with free variables. Secondly, staging annotations, as the term ``annotations'' suggests, are often thought to be orthogonal to the behavior of a program, but when is this formally guaranteed to be the case? I give termination conditions that characterize when this guarantee holds. Finally, do multi-stage languages satisfy extensional facts, for example that functions agreeing on all arguments are equivalent? I develop a sound and complete notion of applicative bisimulation, which can establish not only extensionality but, in principle, any other valid program equivalence as well. These results improve our general understanding of staging and enable us to prove the correctness of complicated multi-stage programs.

This thesis establishes formal equational properties of multi-stage calculi and related proof techniques that support analyses of staged programs. A key promise of staging is to make programs efficient without destroying clarity, thereby reducing the likelihood of bugs. However, few publications rigorously verify that their staged programs indeed behave as intended. In fact, little is known about how staged programs can be verified, or what correctness issues staging introduces. To solve this problem, I show a reduction of the correctness of a staged program to that of an unstaged program. This reduction not only clarifies the effects of staging on program behavior but also eases verification, as unstaged programs are more susceptible to existing reasoning techniques. I also demonstrate that important single-stage reasoning techniques apply to staged programs. These techniques are useful for establishing side conditions for the reduction and for discovering or validating further reasoning principles. / NSF grant CCF-0747431

L’objectif principal de cette thèse est l’étude et la formalisation de nouvelles constructions permettant d’augmenter l’expressivité du filtrage et des langages à base de règles en général. Ceci est motivé par le développement de Tom, un système qui enrichit les langages impératifs comme Java et C avec des constructions de haut niveau comme le filtrage et les stratégies. Une première extension que l’on propose est la notion d’anti-patterns, i.e. des motifs qui peuvent contenir des symboles de complément. Nous définissons de manière formelle la sémantique des anti-patterns dans le cas syntaxique et modulo une théorie équationnelle arbitraire. Puis nous étendons la notion classique de filtrage entre les motifs et les termes clos au filtrage entre les anti-patterns et les termes clos (anti-filtrage). Ensuite, nous proposons plusieurs extensions aux constructions de filtrage fournies par Tom. La condition pour l’application d’une règle devient une conjonction ou disjonction de contraintes de filtrage et d’anti-filtrage ainsi que d’autres types de conditions. Les techniques classiques de compilation du filtrage ne sont pas bien adaptées à ces conditions complexes. On propose donc une nouvelle méthode de compilation basée sur des systèmes de réécriture contrôlés par des stratégies. Nous avons complètement réécrit le compilateur de Tom en utilisant cette technique. Tous ces éléments rassemblés constituent un environnement pour décrire et implémenter des transformations de manière élégante et concise. Pour promouvoir son utilisation dans des projets à grand échelle, on développe une technique pour extraire automatiquement des informations structurelles à partir d’une hiérarchie de classes Java. Cela permet l’intégration du filtrage offert par Tom dans n’importe quelle application Java / The main objective of this thesis is the study of new constructs and formalisms that increase the expressivity of pattern matching and rule based languages in general. This is motivated by the development of Tom, a system that adds high level constructs such as pattern matching and strategies to languages like Java and C. A first extension that we propose is the notion of anti-patterns, i.e. patterns that may contain complement symbols. We define formally the semantics of anti-patterns both in the syntactic case and modulo an arbitrary equational theory. We then extend the classical notion of matching between patterns and ground terms to matching between anti-patterns and ground terms. We further propose several extensions to the matching constructs provided by Tom. Consequently, the condition for the application of a rule becomes a combination of matching and anti-matching constraints together with other types of conditions. Classical compilation techniques for pattern matching are not very well suited for these complex conditions. Therefore we propose a new compilation method based on rewrite systems controlled by strategies, which provides a high level of modularity. Tom’s compiler has been rewritten from scratch using this technique. All this constitutes a software environment for expressing transformations in a clear and concise way. To promote its use in large scale applications, we propose an approach for extracting automatically structural information from arbitrary Java hierarchies. This allows a seamless integration of Tom’s pattern matching facilities in any application

The area of formal analysis of cryptographic protocols has been an active one since the mid 80’s. The idea is to verify communication protocols that use encryption to guarantee secrecy and that use authentication of data to ensure security. Formal methods are used in protocol analysis to provide formal proofs of security, and to uncover bugs and security flaws that in some cases had remained unknown long after the original protocol publication, such as the case of the well known Needham-Schroeder Public Key (NSPK) protocol. In this thesis we tackle problems regarding the three main pillars of protocol verification: modelling capabilities, verifiable properties, and efficiency. This thesis is devoted to investigate advanced features in the analysis of cryptographic protocols tailored to the Maude-NPA tool. This tool is a model-checker for cryptographic protocol analysis that allows for the incorporation of different equational theories and operates in the unbounded session model without the use of data or control abstraction. An important contribution of this thesis is relative to theoretical aspects of protocol verification in Maude-NPA. First, we define a forwards operational semantics, using rewriting logic as the theoretical framework and the Maude programming language as tool support. This is the first time that a forwards rewriting-based semantics is given for Maude-NPA. Second, we also study the problem that arises in cryptographic protocol analysis when it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the protocol equational theory. We also study techniques to extend Maude-NPA capabilities to support the verification of a wider class of protocols and security properties. First, we present a framework to specify and verify sequential protocol compositions in which one or more child protocols make use of information obtained from running a parent protocol. Second, we present a theoretical framework to specify and verify protocol indistinguishability in Maude-NPA. This kind of properties aim to verify that an attacker cannot distinguish between two versions of a protocol: for example, one using one secret and one using another, as it happens in electronic voting protocols. Finally, this thesis contributes to improve the efficiency of protocol verification in Maude-NPA. We define several techniques which drastically reduce the state space, and can often yield a finite state space, so that whether the desired security property holds or not can in fact be decided automatically, in spite of the general undecidability of such problems. / Santiago Pinazo, S. (2015). Advanced Features in Protocol Verification: Theory, Properties, and Efficiency in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/48527