Distributed Ledger Technologies (DLTs), when managed by a few trusted validators, require most but not all of the machinery available in public DLTs. To profit from this s tate of affairs, we inject a PoA (Proof-of-Authority) protocol into Bitcoin, replacing its PoW. Our PoA consensus algorithm-built on top of PBFT and FROST-exhibits Byzantine Fault Tolerance and Confidentiality of the network configuration an d of th e quorum of signers. As such, it may become a modern and safe foundation for payment systems used in stablecoins, sidechains, and CBDCs.

Logic-based Knowledge Graphs (KGs) are gaining momentum in academia and industry thanks to the rise of expressive and efficient languages for Knowledge Representation and Reasoning (KRR). These languages accurately express business rules, through which valuable new knowledge is derived. A versatile and scalable backend reasoner, like Vadalog, a state-of-the-art system for logic-based KGs---based on an extension of Datalog---executes the reasoning. In this demo, we present KG-Roar, a web-based interactive development and navigation environment for logical KGs. The system lets the user augment an input graph database with intensional definitions of new nodes and edges and turn it into a KG, via the metaphor of reasoning widgets---user-defined or off-the-shelf code snippets that capture business definitions in the Vadalog language. Then, the user can seamlessly browse the original and the derived nodes and edges within a "Virtual Knowledge Graph", which is reasoned upon and generated interactively at runtime, thanks to the scalability and responsiveness of Vadalog. KG-Roar is domain-independent but domain aware, as exploration controls are contextually generated based on the intensional definitions. We walk the audience through KG-Roar showcasing the construction of certain business definitions and putting it into action on a real-world financial KG, from our work with the Bank of Italy.

Role-Based Access Control (RBAC) policies are at the core of Cybersecurity as they ease the enforcement of basic security principles, e.g., Least Privilege and Separation of Duties. As ICT systems and business processes evolve, RBAC policies have to be updated to prevent unauthorised access to resources by capturing errors and misalignments between the current policy and reality. However, such update process is a human-intensive activity and it is expected to meet specific constraints. This paper proposes a semi-automatic RBAC maintenance process to fix and refine an RBAC state when “exceptions” and “violations” are detected. Exceptions are permissions some users realise they miss that are instrumental to their job and should be granted as soon as possible, while violations are permissions that have to be revoked since they are no longer required by their current owners. We propose a formalisation for the maintenance process which fixes single and multiple exceptions and violations by balancing two conflicting objectives, i.e., (i) optimising the current RBAC state, and (ii) reducing the transition cost. Our approach is based on a Max-SAT formalisation of the constraint-based optimisation problem, and on PDDL planning to define the transition strategy with minimum cost. Our implementation relies on incomplete Max-SAT solvers and satisficing PDDL planners which provide approximations of optimal solutions. Experiments along with a comparative evaluation show good performance on real-world benchmarks.

In the past decade, many organizations have adopted a Role-Based Access Control model (RBAC) to reduce their administration costs and increase security. The migration to RBAC requires a role engineering phase aimed at generating "good" initial roles starting from direct assignments of permissions to users. For an RBAC approach to be effective, however, it is also necessary to update roles and keep them compliant with the dynamic nature of the business processes; not only this, but errors and misalignments between the current RBAC state and reality need to be promptly detected and fixed. In this paper, we propose a new maintenance process to fix and refine an RBAC state when "exceptions" are detected. Exceptions are permissions some users realize they miss that are instrumental to their job and should be granted as soon as possible. They are catched by a monitoring system as unexpected "access denied" conditions and then validated by the RBAC administrator. The fix we produce aims at balancing two conflicting objectives, i.e., (i) simplifying the current RBAC state, and (ii) reducing the transition cost. Our approach is based on a Max-SAT formalization of this trade-off and it exploits incomplete solvers that quickly provide approximations of optimal solutions. Experiments show good performance on real-world benchmarks.

Formal CAD tools operate on mathematical models describing the sequential behavior of a VLSI design. With the growing size and state-space of modern digital hardware designs, the conciseness of this mathematical model is of paramount importance in extending the scalability of those tools, provided that the compression does not come at the cost of reduced performance. Quantified Boolean Formula satisfiability (QBF) is a powerful generalization of Boolean satisfiability (SAT). It also belongs to the same complexity class as many CAD problems dealing with sequential circuits, which makes it a natural candidate for encoding such problems. This work proposes a succinct QBF encoding for modeling sequential circuit behavior. The encoding is parametrized and further compression is achieved using time-frame windowing. Comprehensive hardware constructions are used to illustrate the proposed encodings. Three notable CAD problems, namely bounded model checking, design debugging and sequential test pattern generation, are encoded as QBF instances to demonstrate the robustness and practicality of the proposed approach. Extensive experiments on OpenCore circuits show memory reductions in the order of 90 percent and demonstrate competitive runtimes compared to state-of-the-art SAT techniques. Furthermore, the number of solved instances is increased by 16 percent. Admittedly, this work encourages further research in the use of QBF in CAD for VLSI.

Many CAD for VLSI techniques use time-frame expansion, also known as the Iterative Logic Array representation, to model the sequential behavior of a system. Replicating industrial- size designs for many time-frames may impose impractically ex- cessive memory requirements. This work proposes a performance- driven, succinct and parametrizable Quantified Boolean Formula (QBF) satisfiability encoding and its hardware implementation for modeling sequential circuit behavior. This encoding is then applied to three notable CAD problems, namely Bounded Model Checking (BMC), sequential test generation and design debugging. Extensive experiments on industrial circuits confirm outstanding run-time and memory gains compared to state-of-the-art techniques, pro- moting the use of QBF in CAD for VLSI.