Category: News

Categories
Honors and Awards News

Best Artifact Award for security verification

The paper “Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2”, coauthored with Hamed Arshad, Ross Horne, Olaf Owe, and Tim Willemse, wins the Best Artifact Award at the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems

This work was part of the PhD thesis of Hamed, and the paper is coauthored by five people (from Luxembourg, Netherlands, University of Oslo, and NTNU). The paper was presented at FORTE during the confederated conferences called DisCoTec 2022 and the new tool called XACML2mCRL2 was demoed to the whole community during the plenary demos session. The tool was given the Best Artifact Award (https://www.discotec.org/2022/programme#discotec-best-artefacts) and was also invited for a special issue of the prestigious Elsevier journal Science of Computer Programming appearing in 2023.

Image showing an overview of the verification tool chain, with our tool in green.

The tool is meant to help verify correctness of access control policies, especially applicable to the health domain where our usecase is taken from (hence the playful title of the paper, “Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2”).

In academia one can use this tool in teaching (it is already used in the MSc course IMT4123 Systems Security at NTNU) or one can build MSc theses topics using the tool for various applications or extensions. More widely, one can use this tool in projects and help industry with their verification tasks.

Categories
Accepted Papers News

Domain Semirings United

Our short paper “Domain Semirings United” coauthored with Uli Fahrenberg, Georg Struth, and Krzysztof Ziemiánski, was accepted by the journal Acta Cybernetica, but will appear only next year (probably in Vol. 25 Nr. 3). In the meantime you can read the paper on the arXiv.

Abstract:

Domain operations on semirings have been axiomatised in two different ways: by a map from an additively idempotent semiring into a boolean subalgebra of the semiring bounded by the additive and multiplicative unit of the semiring, or by an endofunction on a semiring that induces a distributive lattice bounded by the two units as its image. This note presents classes of semirings where these approaches coincide.

Categories
Drafts in Press News

Posets with Interfaces

After quite some time, we have released a long version of our work on “Posets with Interfaces for Concurrent Kleene Algebra“, co-authored with Uli Fahrenberg, Georg Struth, and Krzysztof Ziemiański, which is now being reviewed for a journal.

Abstract:

We introduce posets with interfaces (iposets) and generalise the serial composition of posets to a new gluing composition of iposets. In partial order semantics of concurrency, this amounts to designate events that continue their execution across components. Alternatively, in terms of decomposing concurrent systems, it allows cutting through some events, whereas serial composition may cut through edges only.

We show that iposets under gluing composition form a category, extending the monoid of posets under serial composition, and a 2-category when enriched with a subsumption order and a suitable parallel composition as a lax tensor. This generalises the interchange monoids used in concurrent Kleene algebra.

We also consider gp-iposets, which are generated from singletons by finitary gluing and parallel compositions. We show that the class includes the series-parallel posets as well as the interval orders, which are also well studied in concurrency theory. Finally, we show that not all posets are gp-iposets, exposing several posets that cannot occur as induced substructures of gp-iposets.

Categories
Accepted Papers News

Sculptures in Concurrency

Logical Methods in Computer Science, the most prestigious journal managed solely by the theoretical computer science community, has published our work on Sculptures in Concurrency, co-authored with Uli Fahrenberg, Christopher A. Trotter, and Krzysztof Ziemiański.

Abstract:

We give a formalization of Pratt’s intuitive sculpting process for higher-dimensional automata (HDA). Intuitively, an HDA is a sculpture if it can be embedded in (i.e., sculpted from) a single higher dimensional cell (hypercube). A first important result of this paper is that not all HDA can be sculpted, exemplified through several natural acyclic HDA, one being the famous “broken box” example of van Glabbeek. Moreover, we show that even the natural operation of unfolding is completely unrelated to sculpting, e.g., there are sculptures whose unfoldings cannot be sculpted. We investigate the expressiveness of sculptures, as a proper subclass of HDA, by showing them to be equivalent to regular ST-structures (an event-based counterpart of HDA) and to (regular) Chu spaces over 3 (in their concurrent interpretation given by Pratt). We believe that our results shed new light on the intuitions behind sculpting as a method of modeling concurrent behavior, showing the precise reaches of its expressiveness. Besides expressiveness, we also develop an algorithm to decide whether an HDA can be sculpted. More importantly, we show that sculptures are equivalent to Euclidean cubical complexes (being the geometrical counterpart of our combinatorial definition), which include the popular PV models used for deadlock detection. This exposes a close connection between geometric and combinatorial models for concurrency which may be of use for both areas.