Abstract Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks, and models for concurrency. LL’s cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. This paper formalizes the proof of cut-elimination for focused LL. For that, we propose a set of five cut-rules that allows us to prove cut-elimination directly on the focused system. We also encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have cut-elimination. We then obtain, for free, cut-elimination for first-order classical, intuitionistic, and variants of LL. We also use the LL metatheory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. Hence, we propose a framework that can be used to formalize fundamental properties of logical systems specified as LL theories.

We present a linear logical framework implemented within the Hybrid system [Felty and Momigliano 2012]. Hybrid is designed to support the use of higher-order abstract syntax for representing and reasoning about formal systems, implemented in the Coq Proof Assistant. In this work, we extend the system with a linear specification logic, which provides infrastructure for reasoning directly about object languages with linear features.

The genesis of this special issue was in a meeting that took place at Université Paris Diderot on December 15 and 16, 2016. Dale Miller, Professor at École polytechnique, had turned 60 a few days earlier. In a career spanning over three decades and in work conducted in collaboration with several students and colleagues, Dale had had a significant influence in an area that can be described as structural proof theory and its application to computation and reasoning. In recognition of this fact, several of his collaborators thought it appropriate to celebrate the occasion by organizing a symposium on topics broadly connected to his areas of interest and achievements. The meeting was a success in several senses: it was attended by over 35 people, there were 15 technical presentations describing new results, and, quite gratifyingly, we managed to spring the event as a complete surprise to Dale.

A variety of logical frameworks supports the use of higher order abstract syntax in representing formal systems. Although these systems seem superficially the same, they differ in a variety of ways, for example, how they handle acontextof assumptions and which theorems about a given formal system can be concisely expressed and proved. Our contributions in this paper are two-fold: (1) We develop a common infrastructure and language for describing benchmarks for systems supporting reasoning with binders, and (2) we present several concrete benchmarks, which highlight a variety of different aspects of reasoning within a context of assumptions. Our work provides the background for the qualitative comparison of different systems that we have completed in a separate paper. It also allows us to outline future fundamental research questions regarding the design and implementation of meta-reasoning systems.

We present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control policies. We define formal semantics for ACCPL and use the Coq Proof Assistant to state theorems about this semantics, to develop proofs for those theorems and to machine-check the proofs ensuring correctness guarantees are provided. The main design goal for ACCPL is the ability to reason about the policies written in ACCPL with respect to specific questions such as safety. In addition, ACCPL and the established proofs are integrated such that extensions to expressive power may be explored by also extending identifiable proof statements in the direction of the added expressivity. To this end, ACCPL is small (the syntax and the semantics of ACCPL only take a few pages to describe), although we believe ACCPL supports the core features of many access-control policy languages.

Policy specification languages such as XACML often provide mechanisms to resolve dynamic conflicts that occur when trying to determine if a request should be permitted or denied access by a policy. Examples include "deny-overrides" or "first-applicable." Such algorithms are primitive and potentially a risk for corporate computer security. While they can be useful for resolving dynamic conflicts, they are not justified for conflicts that can be easily detected statically. It is better to find those at compile time and remove them before run time. Many different approaches have been used for static conflict detection. However, most of them do not scale well because they rely on pair-wise comparison of the access control logic of policies and rules. We propose an extension of a Prolog-based expert system approach due to Eronen and Zitting. This approach uses constraint logic programming techniques (CLP), which are well-adapted to hierarchical XACML policy logic and avoid pair-wise comparisons altogether by taking advantage of Prolog's built-in powerful indexing system. We demonstrate that expert systems can indeed detect conflicts statically, even those that are generally believed to only be detectable at run time, by inferring the values of attributes that would cause a conflict. As a result, relying on the XACML policy combining algorithms can be avoided in most cases except in federated systems. Finally we provide performance measurements for two different architectures represented in Prolog and give some analysis.

We describe the formalization of a correctness proof for a conflict detection algorithm for XACML (eXtensible Access Control Markup Language). XACML is a standardized declarative access control policy language that is increasingly used in industry. In practice it is common for rule sets to grow large, and contain unintended errors, often due to conflicting rules. A conflict occurs in a policy when one rule permits a request and another denies that same request. Such errors can lead to serious risks involving both allowing access to an unauthorized user as well as denying access to someone who needs it. Removing conflicts is thus an important aspect of debugging policies, and the use of a verified algorithm provides the highest assurance in a domain where security is important. In this paper, we focus on several complex XACML constructs, including time ranges and integer intervals, as well as ways to combine any number of functions using the boolean operators and, or, and not. The latter are the most complex, and add significant expressive power to the language. We propose an algorithm to find conflicts and then use the Coq Proof Assistant to prove the algorithm correct. We develop a library of tactics to help automate the proof.

XACML (extensible Access Control Mark-up Language) is a declarative access control policy language that has unique language constructs for factoring out access control logic. These constructs make the specification of access control requirements more compact than decision trees, which can be considered the most natural way to specify access control logic. However, many publications report that performance of XACML policy decision point (PDP) engines is greatly affected by the structure of policy sets. In this paper we first explore the causes of potential inefficiencies of XACML policies, and then propose a procedure to re-structure policy sets vertically by modifying the distribution of access control logic among different configurations of structural elements, in order to remove much of this inefficiency. This is in contrast to horizontal re-ordering of constant structural elements. Our procedure can be applied regardless of the complexity and structure of the original policy set. We also compare the performance of policy sets that take advantage of the expressive power of XACML targets to decision trees.

Policy administrators increasingly face the challenge of managing large policy bases, and this need becomes more acute with the growing importance of fine-grained access control models, e.g. ABAC. We have shown in previous work that simple policies mostly based on conjunctions of single attribute conditions, can be merged into more complex conditions composed of combinations of conjunctions and disjunctions of attribute/value pairs. Here, we propose an algorithm that uses a recursive process of subsumption applied on the original set of policies that results in a complex and short policy, often significantly compressing the original policy. We present this algorithm, and discuss the advantages of this approach, i.e. its performance when working on the policy structures encountered in real-life policy sets, its scalability, and its ability to deal with large alphabet sets.

As applications requiring access control and the environments in which they operate in become more complex, an acute need for better ways to manage access control rules has arisen. Decentralized access control, for example, requires sophisticated techniques for conflict detection and for managing rules across multiple applications with different rule formats. XACML is an OASIS standard whose interoperability qualities help in solving the latter problem. XACML has its own limitations, however. In particular, although it has the expressive power to specify very complex conditions like those needed in the ABAC (Attribute Based Access Control) model, users tend to avoid using its full power because of its verbosity. In this paper, we show how a non-technical notation we have proposed in our earlier work resolves this difficulty and allows users to work with a very compact and readable form of XACML rules, thus allowing them to take advantage of XACML's full expressive power. This expressive power can be exploited to write policies that are better organized. It can be easier, for example, to write a single possibly complex rule to cover a particular aspect of a policy as opposed to distributing the complexity over several rules with simpler conditions. As a result, policies are smaller, more compact, and easier to understand. Policy development becomes more manageable, allowing users to concentrate on the more central issue of choosing the model (RBAC, ABAC, PBAC or other) that is best suited to a particular application and policy. We show that using the full expressive power to better organize policies has a significant positive impact on PDP performance.

Proof-carrying code (PCC) is a technique that addresses the problem of mobile code safety. It is a mechanism in which a code producer provides both code and a proof certifying that the code will run safely on a code consumer's machine. The code consumer or the host system will validate the proof against a safety policy before executing the source code. Foundational proof-carrying code (FPCC) aims to minimize the amount of code that must be trusted (the “trusted computing base” or TCB) with the goal of providing more flexibility and increased security. In both PCC and FPCC, the verification-condition generator (VCG) constructs the statement of the safety theorem from the source code, and is an important part of the TCB. This paper presents an implementation of a VCG based on a sound set of Hoare-style rules for machine instructions in the context of FPCC. The implementation in OCaml is described and examples illustrating the approach are given. The output of our VCG is a list of verification conditions that are directly inserted into a proof script that serves as input to the Coq proof assistant, and represents an important part of the safety proofs of our programs. We also present examples showing how these verification conditions are used to complete the proofs of safety. This work represents an important step in automating proofs for PCC.

Managing access control policies is a complex task. We argue that much of the complexity is unnecessary and mostly due to historical reasons. There are number of legacy policy specification languages that all have limitations of some kind. These limitations have forced policy implementers to use certain styles of writing policies, often resulting in inconsistencies. The detection and resolution of these inconsistencies has been widely researched and many solutions have been found. This paper highlights new possibilities for avoiding inconsistencies, drawing on the expressive power allowed in the condition field of rules in modern languages such as XACML. In particular, we show that making use of this expressive power has many advantages-it allows organizations to considerably reduce the number of policies and rules required to protect company assets; it provides improved views and summaries of related policies; and it allows increased scalability of analysis tools, such as tools that detect inconsistencies and tools that perform audits to verify compliance to regulations. Such tools are increasingly important in the current environment where the number of regulations governing company security continues to grow. In addition, we show how our user-friendly representation for the XACML language facilitates the use of complex conditions by increasing their readability. This increased readability has the additional benefit of allowing non-technical users to better understand the implementation of their policies. These factors all contribute to a lower risk of inconsistencies in policies.

Hybrid is a system developed to specify and reason about logics, programming languages, and other formal systems expressed in higher-order abstract syntax (HOAS). An important goal of Hybrid is to exploit the advantages of HOAS within the well-understood setting of higher-order logic as implemented by systems such as Isabelle and Coq. In this paper, we add new capabilities for reasoning by induction on encodings of object-level inference rules. Elegant and succinct specifications of such inference rules can often be given using hypothetical and parametric judgments, which are represented by embedded implication and universal quantification. Induction over such judgments is well-known to be problematic. In previous work, we showed how to express this kind of judgment using a two-level approach, but reasoning by induction on such judgments was restricted to closed terms. The new capabilities we add include techniques for adding arbitrary "new" variables to contexts and inductively reasoning about open terms. Very little overhead is required, namely a small library of definitions and lemmas, yet the reasoning power of the system and the class of properties that can be proved is significantly increased. We illustrate the approach using PCF, a simple programming language that serves as the core of a variety of functional languages. We encode the typing judgment, and prove by induction on this judgment that well-typed PCF terms have unique types.

This article introduces our new approach to program rep-resentation for genetic programming (GP). We replace the usual s-expression representation scheme by a strongly-typed abstraction-based representation scheme. This allows us to represent many typical computational structures by abstrac-tions rather than by functions defined in the GP system’s terminal set. The result is a generic GP system that is able to express programming structures such as recursion and data types without explicit definitions. We demonstrate the expressive power of this approach by evolving simple boolean programs without defining a set of terminals. We also evolve programs that exhibit recursive behavior without explicitly defining recursion specific syntax in the terminal set. In this article, we present our approach and experimen-tal results.

Static type systems in programming languages allow many errors to be detected at compile time that wouldn't be detected until runtime otherwise. Dependent types are more expressive than the type systems in most programming languages, so languages that have them should allow programmers to detect more errors earlier. In this paper, using the Twelf system, we show that dependent types in the logic programming setting can be used to ensure partial correctness of programs which implement theorem provers, and thus avoid runtime errors in proof search and proof construction. We present two examples: a tactic-style interactive theorem prover and a union-find decision procedure.

$\lambda$ Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage ( $\lambda$ Prolog). We discuss both the Terzo and Teyjus implementations of $\lambda$ Prolog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.

Large software systems, especially in the telecommunications field, are often specified as a collection of features. We present a formal specification language for describing features, and a method of automatically detecting conflicts ("undesirable interactions") amongst features at the specification stage. Conflict detection at this early stage can help prevent costly and time consuming problem fixes during implementation. Features are specified using temporal logic; two features conflict essentially if their specifications are mutually inconsistent under axioms about the underlying system behavior. We show how this inconsistency check may be performed automatically with existing model checking tools. In addition, the model checking tools can be used to provide witness scenarios, both when two features conflict as well as when the features are mutually consistent. Both types of witnesses are useful for refining the specifications. We have implemented a conflict detection tool, FIX (Feature Interaction eXtractor), which uses the model checker COSPAN for the inconsistency check. We describe our experience in applying this tool to a collection of telecommunications feature specifications obtained from the Telcordia (Bellcore) standards. Using FIX, we were able to detect most known interactions and some new ones, fully automatically, in a few hours processing time.

Proof-carrying code is a framework for proving the safety of machine-language programs with a machinecheckable proof. Such proofs have previously defined type-checking rules as part of the logic. We show a universal type framework for proof-carrying code that will allow a code producer to choose a programming language, prove the type rules for that language as lemmas in higher-order logic, then use those lemmas to prove the safety of a particular program. We show how to handle traversal, allocation, and initialization of values in a wide variety of types, including functions, records, unions, existentials, and covariant recursive types. 1 Introduction When a host computer runs an untrusted program, the host may want some assurance that the program does no harm: does not access unauthorized resources, read private data, or overwrite valuable data. Proof-carrying code [Nec97] is a technique for providing such assurances. With PCC, the host -- called the "code consumer" -- specifies a sa...

We show how a procedure developed by Bledsoe for automatically finding substitution instances for set variables in higher-order logic can be adapted to provide increased automation in proof search in the Calculus of Constructions (CC). Bledsoe's procedure operates on an extension of first-order logic that allows existential quantification over set variables. This class of variables can also be identified in CC. The existence of a correspondence between higher-order logic and higher-order type theories such as CC is well-known. CC can be viewed as an extension of higher-order logic where the basic terms of the language, the simply-typed λ-terms, are replaced with terms containing dependent types. We show how Bledsoe's techniques can be incorporated into a reformulation of a search procedure for CC given by Dowek and extended to handle terms with dependent types. We introduce a notion of search context for CC which allows us to separate the operations of assumption introduction and backchaining. Search contexts allow a smooth integration of the step which finds solutions to set variables. We discuss how the procedure can be restricted to obtain procedures for set variable instantiation in sublanguages of CC such as the Logical Framework (LF) and higher-order hereditary Harrop formulas (hohh). The latter serves as the logical foundation of the λProlog logic programming language.

Abstract. SCI – Scalable Coherent Interface – is an IEEE standard for specifying communication between multiprocessors in a shared memory model. In this paper we model part of SCI by a program written in a UNITY-like programming language. This part of SCI is formally specified in Manna and Pnueli's Linear Time Temporal Logic (LTL). We give a sketch of our proof that the program satisfies its specification. The proof has been carried out within LTL. It uses history variables. Structuring of the proof has been achieved by careful formulation of lemmata and the use of auxiliary predicates as an abstraction mechanism.

The author presents an encoding of the calculus of constructions (CC) in a higher-order intuitionistic logic (I) in a direct way, so that correct typing in CC corresponds to intuitionistic provability in a sequent calculus for I. In addition, she demonstrates a direct correspondence between proofs in these two systems. The logic I is an extension of hereditary Harrop formulas (hh), which serve as the logical foundation of the logic programming language lambda Prolog. Like hh, I has the uniform proof property, which allows a complete nondeterministic search procedure to be described in a straightforward manner. Via the encoding, this search procedure provides a goal directed description of proof checking and proof search in CC.>