The ability to exchange data while maintaining sovereignty is fundamental to emerging decentralized data-driven ecosystems. Data sovereignty refers to the entity's capability to be self-determined concerning data usage. As such, a data usage control system (UCON) is critical for sovereignty. UCON, a generalization of attribute-based access control, enforces continuous authorization, allowing attribute mutability after access is granted. In theory, UCON comprises a policy language to express constraints and obligations of data usage, and a technology to evaluate and enforce them. In practice, realizing the above is challenging and poses trust concerns. Partly, this is due to the complexity of UCON (continuous authorization, obligations) and the advanced usage constraints (stemming from, e.g., regulations or business contracts) combined with the decentralized nature of data ecosystems that allow different actors (e.g., data provider, security engineers) to author policies, and operate UCON. To that end, we propose to aid actors with automated policy analysis and verification methods. We present a new policy analysis method based on the combination of symbolic execution for policy evaluation and SMT solving to compute concrete scenarios answering queries on the policies. Our approach supports symbolic queries, where attribute values may be concrete values, a range of values, or symbolic variables. We also propose a monitoring approach using RTLola tool to verify the correctness of UCON's behavior in terms of decisions, obligations, and user-specified properties. To monitor obligations, we define their essential parameters and show how to monitor their fulfillment based on the configuration. We also present eight templates that allow users to generate the most important properties for monitoring UCON.

Modern system architectures require sophisticated access and usage control mechanisms. The need stems from demanding requirements for security, data sovereignty and privacy regulations, as well as the challenges presented by architectural approaches like zero trust networking. Usage control systems provide one approach to encapsulate and manage the complexities related to access and usage control. In order to trust a usage control system, it is essential to ensure that usage control policies express the intended properties and are enforced correctly. To achieve this, we need a precise specification of the intended behavior of a usage control system. For attribute-based access control, the XACML standard is a sufficient specification of the behavior of policies. Usage control models, such as UCON, extend access control with features for continuous authorization based on mutability of attribute values. This adds significant complexity to the problem of specifying the intended behavior. In this paper, we identify challenges with specifying a practical usage control system regarding continuous control, obligations, and concurrency aspects. We describe an approach to specifying the UCON+ model of Dimitrakos et al. and outline an implementation of the specification with Answer Set Programming.

This is the second part of a two-part special issue dedicated to the memory of our friend and colleague, Martin Hofmann.The first part was published as Mathematical Structures in Computer Science (2021), 31(9).On 21 January 2018, Martin Hofmann died in a tragic mountain hiking accident in Japan.He was there to attend a workshop at NII Shonan and arrived early for the workshop in order to spend a day climbing Mount Nikkō-Shirane.On his way down from the 2578 m summit, he was caught in a severe snowstorm and lost his way back to safety.

We describe the categorical semantics for a simply typed variant and a simplified dependently typed variant of Cocon , a contextual modal type theory where the box modality mediates between the weak function space that is used to represent higher-order abstract syntax (HOAS) trees and the strong function space that describes (recursive) computations about them. What makes Cocon different from standard type theories is the presence of first-class contexts and contextual objects to describe syntax trees that are closed with respect to a given context of assumptions. Following M. Hofmann’s work, we use a presheaf model to characterise HOAS trees. Surprisingly, this model already provides the necessary structure to also model Cocon . In particular, we can capture the contextual objects of Cocon using a comonad ♭ that restricts presheaves to their closed elements. This gives a simple semantic characterisation of the invariants of contextual types (e.g. substitution invariance) and identifies Cocon as a type-theoretic syntax of presheaf models. We further extend this characterisation to dependent types using categories with families and show that we can model a fragment of Cocon without recursor in the Fitch-style dependent modal type theory presented by Birkedal et al.

We introduce a generic type system for Featherweight Java (FJ) that is parametrized with a monad-like structure, and prove a uniform soundness theorem. Its instances include some region type systems studied by Martin Hofmann et al. as well as a new one that performs more precise analysis of trace-based properties. Their soundness is guaranteed by the uniform theorem. We only need to verify some natural conditions. Instead of refining the FJ type system as in the previous work, our region type system is separate from the FJ type system, making it simpler and also easier to move to larger fragments of Java. Moreover, the uniform framework helps to avoid redundant work on the meta-theory when extending the system to cover other language features such as exception handling.

A common approach to improve software quality is to use programming guidelines to avoid common kinds of errors. In this paper, we consider the problem of enforcing guidelines for Featherweight Java (FJ). We formalize guidelines as sets of finite or infinite execution traces and develop a region-based type and effect system for FJ that can enforce such guidelines. We build on the work by Erbatur, Hofmann and Zălinescu, who presented a type system for verifying the finite event traces of terminating FJ programs. We refine this type system, separating region typing from FJ typing, and use ideas of Hofmann and Chen to extend it to capture also infinite traces produced by non-terminating programs. Our type and effect system can express properties of both finite and infinite traces and can compute information about the possible infinite traces of FJ programs. Specifically, the set of infinite traces of a method is constructed as the greatest fixed point of the operator which calculates the possible traces of method bodies. Our type inference algorithm is realized by working with the finitary abstraction of the system based on Büchi automata.

This is the first part of a two-part special issue of Mathematical Structures in Computer Science dedicated to the memory of our friend and colleague, Martin Hofmann.On 21 January 2018, Martin Hofmann died in a tragic mountain hiking accident in Japan.He was there to attend a workshop at NII Shonan and arrived early for the workshop in order to spend a day climbing Mount Nikkō-Shirane.On his way down from the 2578-m summit, he was caught in a severe snowstorm and lost his way back to safety.

Abstract We describe a category-theoretic semantics for a simply typed variant of Cocon, a contextual modal type theory where the box modality mediates between the weak function space that is used to represent higher-order abstract syntax (HOAS) trees and the strong function space that describes (recursive) computations about them. What makes Cocon different from standard type theories is the presence of first-class contexts and contextual objects to describe syntax trees that are closed with respect to a given context of assumptions. Following M. Hofmann’s work, we use a presheaf model to characterise HOAS trees. Surprisingly, this model already provides the necessary structure to also model Cocon. In particular, we can capture the contextual objects of Cocon using a comonad $$\flat $$ ♭ that restricts presheaves to their closed elements. This gives a simple semantic characterisation of the invariants of contextual types (e.g. substitution invariance) and identifies Cocon as a type-theoretic syntax of presheaf models. We express our category-theoretic constructions by using a modal internal type theory that is implemented in Agda-Flat.

We study the problem of translating from call-by-value pcf to a first-order low-level language. Such translations are typically defined by induction on the structure of the source term. Each sub-term is translated to a low-level program fragment and the translation of the whole term is a composition of these fragments. It is desirable to follow this compositional approach also in reasoning about such translations, e.g. to show correctness of the translation by verifying the low-level fragments individually. In this paper, we define a defunctionalisation method in which the low-level program fragments are considered as little modules with a well-defined interface. We show correctness of the translation by decomposing it into a number of steps that each allows compositional reasoning. The main step is a typed closure conversion that translates pcf into a calculus based on interaction semantics. It takes into account low-level information, e.g. on closure representation and stack shape, that is obtained by global program analysis. We capture such information using an annotated type system for pcf and show that suitable annotations can be computed by type inference.

Type systems that allow control over low-level compilation details have been developed in the context of resource aware compilation, e.g. for circuit synthesis or for programming with logarithmic space. It was recently observed that some compilation techniques developed in this context, while motivated by capturing certain resource usage restrictions, are closely related to standard compilation techniques, such as CPS translation and defunctionalization. Previous results of this kind suggest to investigate type systems for resource aware compilation more generally with regard to their applicability to structuring general low-level languages, e.g. as used in compilers.

Many logspace algorithms are naturally described as programs that operate on a structured input (e.g., a graph), that store in memory only a constant number of pointers (e.g., to graph nodes) and that do not use pointer arithmetic. Such “pure pointer algorithms” thus are a useful abstraction for studying the nature of logspace-computation. In this article, we introduce a formal class purple of pure pointer programs and study them on locally ordered graphs. Existing classes of pointer algorithms, such as Jumping Automata on Graphs (jags) or Deterministic Transitive Closure (dtc) logic, often exclude simple programs. purple subsumes these classes and allows for a natural representation of many graph algorithms that access the input graph using a constant number of pure pointers. It does so by providing a primitive for iterating an algorithm over all nodes of the input graph in an unspecified order. Since pointers are given as an abstract data type rather than as binary digits we expect that logarithmic-size worktapes cannot be encoded using pointers as is done, for example, in totally ordered dtc-logic. We show that this is indeed the case by proving that the property “the number of nodes is a power of two,” which is in logspace, is not representable in purple.

Pointer programs are a model of structured computation within LOGSPACE. They capture the common description of LOGSPACE algorithms as programs that take as input some structured data (e.g. a graph) and that store in memory only a constant number of pointers to the input (e.g. to the graph nodes). In this paper we study undirected s-t-reachability for a class of pure pointer programs in which one can work with a constant number of abstract pointers, but not with arbitrary data, such as memory registers of logarithmic size. In earlier work we have formalised this class as a programming language PURPLE that features a for all-loop for iterating over the input structure and thus subsumes other formalisations of pure pointer programs, such as Jumping Automata on Graphs JAGs and Deterministic Transitive Closure logic (DTC-logic) for locally ordered graphs. In this paper we show that PURPLE cannot decide undirected s-t-reachability, even though there does exist a LOGSPACE-algorithm for this problem by Reingold's theorem. As a corollary we obtain that DTC-logic for locally ordered graphs cannot express undirected s-t-reachability.

A number of complexity classes, most notably PTIME, have been characterised by sub-systems of linear logic. In this paper we show that the functions computable in logarithmic space can also be characterised by a restricted version of linear logic. We introduce stratified bounded affine logic (SBAL), a restricted version of bounded linear logic, in which not only the modality, but also the universal quantifier is bounded by a resource polynomial. We show that the proofs of certain sequents in SBAL represent exactly the functions computable logarithmic space. The proof that SBAL-proofs can be compiled to LOGSPACE functions rests on modelling computation by interaction dialogues in the style of game semantics. We formulate the compilation of SBAL-proofs to space-efficient programs as an interpretation in a realisability model, in which realisers are taken from a geometry of interaction situation.