BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Flemming Nielson

Flemming Nielson contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer ScienceCryptography and SecurityProgramming LanguagesDistributed, Parallel, and Cluster ComputingFormal Languages and Automata TheoryInformation Theorymath.ITNetworking and Internet ArchitecturePerformanceSystems and Control

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
16works
0followers
10topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

16 published item(s)

preprint2016arXiv

A Theory of Available-by-Design Communicating Systems

Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Starting from a global specification (choreography) one can generate distributed implementations. The advantages of this top-down approach lie in the correctness-by-design principle, where implementations (endpoints) generated from a choreography behave according to the strict control flow described in the choreography, and do not deadlock. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where not all endpoints are always available. We introduce the Global Quality Calculus ($GC_q$), a variant of choreographic programming for the description of communication systems where some of the components involved in a communication might fail. GCq features novel operators for multiparty, partial and collective communications. This paper studies the nature of failure-aware communication: First, we introduce $GC_q$ syntax, semantics and examples of its use. The interplay between failures and collective communications in a choreography can lead to choreographies that cannot progress due to absence of resources. In our second contribution, we provide a type system that ensures that choreographies can be realized despite changing availability conditions. A specification in $GC_q$ guides the implementation of distributed endpoints when paired with global (session) types. Our third contribution provides an endpoint-projection based methodology for the generation of failure-aware distributed processes. We show the correctness of the projection, and that well-typed choreographies with availability considerations enjoy progress.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

A Framework for Hybrid Systems with Denial-of-Service Security Attack

Hybrid systems are integrations of discrete computation and continuous physical evolution. The physical components of such systems introduce safety requirements, the achievement of which asks for the correct monitoring and control from the discrete controllers. However, due to denial-of-service security attack, the expected information from the controllers is not received and as a consequence the physical systems may fail to behave as expected. This paper proposes a formal framework for expressing denial-of-service security attack in hybrid systems. As a virtue, a physical system is able to plan for reasonable behavior in case the ideal control fails due to unreliable communication, in such a way that the safety of the system upon denial-of-service is still guaranteed. In the context of the modeling language, we develop an inference system for verifying safety of hybrid systems, without putting any assumptions on how the environments behave. Based on the inference system, we implement an interactive theorem prover and have applied it to check an example taken from train control system.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL^*. Various behavioral equivalences are proposed, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the equivalences are well-known to be sound, but not complete with respect to the logical equivalences induced by PCTL or PCTL*. The desire of a both sound and complete behavioral equivalence has been pointed out by Segala in 1995, but remains open throughout the years. In this paper we introduce novel notions of strong bisimulation relations, which characterize PCTL and PCTL* exactly. We extend weak bisimulations that characterize PCTL and PCTL* without next operator, respectively. Further, we also extend the framework to simulation preorders. Thus, our paper bridges the gap between logical and behavioral equivalences and preorders in this setting.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Design-Efficiency in Security

In this document, we present our applied results on balancing security and performance using a running example, which is based on sensor networks. These results are forming a basis for a new approach to balance security and performance, and therefore provide design-efficiency of key updates. We employ probabilistic model checking approach and present our modelling and analysis study using PRISM model checker.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Pushdown Systems for Monotone Frameworks

Monotone frameworks is one of the most successful frameworks for intraprocedural data flow analysis extending the traditional class of bitvector frameworks (like live variables and available expressions). Weighted pushdown systems is similarly one of the most general frameworks for interprocedural analysis of programs. However, it makes use of idempotent semirings to represent the sets of properties and unfortunately they do not admit analyses whose transfer functions are not strict (e.g., classical bitvector frameworks). This motivates the development of algorithms for backward and forward reachability of pushdown systems using sets of properties forming so-called flow algebras that weaken some of the assumptions of idempotent semirings. In particular they do admit the bitvector frameworks, monotone frameworks, as well as idempotent semirings. We show that the algorithms are sound under mild assumptions on the flow algebras, mainly that the set of properties constitutes a join semi-lattice, and complete provided that the transfer functions are suitably distributive (but not necessarily strict).

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

XACML 3.0 in Answer Set Programming

We present a systematic technique for transforming XACML 3.0 policies in Answer Set Programming (ASP). We show that the resulting logic program has a unique answer set that directly corresponds to our formalisation of the standard semantics of XACML 3.0 from Ramli et. al. We demonstrate how our results make it possible to use off-the-shelf ASP solvers to formally verify properties of access control policies represented in XACML, such as checking the completeness of a set of access control policies and verifying policy properties.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Efficient CSL Model Checking Using Stratification

For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential complexity. In 2000, Baier, Haverkort, Hermanns and Katoen presented an efficient polynomial-time approximation algorithm for the sublogic in which only binary until is allowed. In this paper, we propose such an efficient polynomial-time approximation algorithm for full CSL. The key to our method is the notion of stratified CTMCs with respect to the CSL property to be checked. On a stratified CTMC, the probability to satisfy a CSL path formula can be approximated by a transient analysis in polynomial time (using uniformization). We present a measure-preserving, linear-time and -space transformation of any CTMC into an equivalent, stratified one. This makes the present work the centerpiece of a broadly applicable full CSL model checker. Recently, the decision algorithm by Aziz et al. was shown to work only for stratified CTMCs. As an additional contribution, our measure-preserving transformation can be used to ensure the decidability for general CTMCs.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Lattice based Least Fixed Point Logic

As software systems become more complex, there is an increasing need for new static analyses. Thanks to the declarative style, logic programming is an attractive formalism for specifying them. However, prior work on using logic programming for static analysis focused on analyses defined over some powerset domain, which is quite limiting. In this paper we present a logic that lifts this restriction, called Lattice based Least Fixed Point Logic (LLFP), that allows interpretations over any complete lattice satisfying Ascending Chain Condition. The main theoretical contribution is a Moore Family result that guarantees that there always is a unique least solution for a given problem. Another contribution is the development of solving algorithm that computes the least model of LLFP formulae guaranteed by the Moore Family result.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Layered Fixed Point Logic

We present a logic for the specification of static analysis problems that goes beyond the logics traditionally used. Its most prominent feature is the direct support for both inductive computations of behaviors as well as co-inductive specifications of properties. Two main theoretical contributions are a Moore Family result and a parametrized worst case time complexity result. We show that the logic and the associated solver can be used for rapid prototyping and illustrate a wide variety of applications within Static Analysis, Constraint Satisfaction Problems and Model Checking. In all cases the complexity result specializes to the worst case time complexity of the classical methods.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Modelling Chinese Smart Grid: A Stochastic Model Checking Case Study

Cyber-physical systems integrate information and communication technology functions to the physical elements of a system for monitoring and controlling purposes. The conversion of traditional power grid into a smart grid, a fundamental example of a cyber-physical system, raises a number of issues that require novel methods and applications. In this context, an important issue is the verification of certain quantitative properties of the system. In this technical report, we consider a specific Chinese Smart Grid implementation and try to address the verification problem for certain quantitative properties including performance and battery consumption. We employ stochastic model checking approach and present our modelling and analysis study using PRISM model checker.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Optimizing ZigBee Security using Stochastic Model Checking

ZigBee is a fairly new but promising wireless sensor network standard that offers the advantages of simple and low resource communication. Nevertheless, security is of great concern to ZigBee, and enhancements are prescribed in the latest ZigBee specication: ZigBee-2007. In this technical report, we identify an important gap in the specification on key updates, and present a methodology for determining optimal key update policies and security parameters. We exploit the stochastic model checking approach using the probabilistic model checker PRISM, and assess the security needs for realistic application scenarios.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Roadmap Document on Stochastic Analysis

This document was prepared as part of the MT-LAB research centre. The research centre studies the Modelling of Information Technology and is a VKR Centre of Excellence funded for five years by the VILLUM Foundation. You can read more about MT-LAB at its webpage www.MT-LAB.dk. The goal of the document is to serve as an introduction to new PhD students addressing the research goals of MT-LAB. As such it aims to provide an overview of a number of selected approaches to the modelling of stochastic systems. It should be readable not only by computers scientists with a background in formal methods but also by PhD students in stochastics that are interested in understanding the computer science approach to stochastic model checking. We have no intention of being encyclopedic in our treatment of the approaches or the literature. Rather we have made the selection of material based on the competences of the groups involved in or closely affiliated to MT-LAB, so as to ease the task of the PhD students in navigating an otherwise vast amount of literature. We have decided to publish the document in case other young researchers may find it helpful. The list of authors reflect those that have at times played a significant role in the production of the document.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Secondary use of data in EHR systems

We show how to use aspect-oriented programming to separate security and trust issues from the logical design of mobile, distributed systems. The main challenge is how to enforce various types of security policies, in particular predictive access control policies - policies based on the future behavior of a program. A novel feature of our approach is that advice is able to analyze the future use of data. We consider a number of different security policies, concerning both primary and secondary use of data, some of which can only be enforced by analysis of process continuations.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

A Stochastic Broadcast Pi-Calculus

In this paper we propose a stochastic broadcast PI-calculus which can be used to model server-client based systems where synchronization is always governed by only one participant. Therefore, there is no need to determine the joint synchronization rates. We also take immediate transitions into account which is useful to model behaviors with no impact on the temporal properties of a system. Since immediate transitions may introduce non-determinism, we will show how these non-determinism can be resolved, and as result a valid CTMC will be obtained finally. Also some practical examples are given to show the application of this calculus.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

The Logic of XACML - Extended

We study the international standard XACML 3.0 for describing security access control policy in a compositional way. Our main contribution is to derive a logic that precisely captures the idea behind the standard and to formally define the semantics of the policy combining algorithms of XACML. To guard against modelling artefacts we provide an alternative way of characterizing the policy combining algorithms and we formally prove the equivalence of these approaches. This allows us to pinpoint the shortcoming of previous approaches to formalization based either on Belnap logic or on D-algebra.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

History-sensitive versus future-sensitive approaches to security in distributed systems

We consider the use of aspect-oriented techniques as a flexible way to deal with security policies in distributed systems. Recent work suggests to use aspects for analysing the future behaviour of programs and to make access control decisions based on this; this gives the flavour of dealing with information flow rather than mere access control. We show in this paper that it is beneficial to augment this approach with history-based components as is the traditional approach in reference monitor-based approaches to mandatory access control. Our developments are performed in an aspect-oriented coordination language aiming to describe the Bell-LaPadula policy as elegantly as possible. Furthermore, the resulting language has the capability of combining both history- and future-sensitive policies, providing even more flexibility and power.

0 citations0 reviewsNo code linkedOpen access