547 research outputs found
Time dependent policy-based access control
No full textAccess control policies are essential to determine who is allowed to access data in a system without compromising the data's security. However, applications inside a distributed environment may require those policies to be dependent on the actual content of the data, the flow of information, while also on other attributes of the environment such as the time. In this paper, we use systems of Timed Automata to model distributed systems and we present a logic in which one can express time-dependent policies for access control. We show how a fragment of our logic can be reduced to a logic that current model checkers for Timed Automata such as UPPAAL can handle and we present a translator that performs this reduction. We then use our translator and UPPAAL to enforce time-dependent policy-based access control on an example application from the aerospace industry
Semantics, Logics, and Calculi:Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
No full textHanne Riis Nielson and Flemming Nielson turned 60 in 2014 and 2015, respectively. Congratulations! To celebrate the 60th birthdays, and to honor the birthday children, a colloquium was held at the Technical University of Denmark on January 8, 2016, to deliver the Festschrift and presentations of most contributions as our birthday presents.This volume is dedicated to Hanne and Flemming and to their work. The Festschrift features contributions from colleagues who have worked together with Hanne and Flemming through their scientific life.We would like to thank all the contributors to this Festschrift — for their hard work, for their both scientifically interesting and individual articles, as well as for their enthusiasm to contribute. The mix of articles resembles very nicely the impressively wide area in which Hanne and Flemming have worked and made fundamental contributions. Both the Festschrift and the colloquium were a wonderful way to celebrate them.Our thanks also go to all the reviewers whose support made excellent articles even better. We are also indebted to Alfred Hofmann at Springer for his feedback and advice on our project, and to Anna Kramer from Springer for her fast responses to all our questions about Festschrifts and all matters around them
Static analysis of a Model of the LDL degradation pathway
No full textBioAmbients is a derivative of mobile ambients that has shown promise of describing interesting features of the behaviour of biological systems. As for other ambient calculi static program analysis can be used to compute safe approximations of the behavior of modelled systems. We use these tools to model and analyse the production of cholesterol in living cells and show that we are able to pinpoint the difference in behaviour between models of healthy systems and models of mutated systems giving rise to known diseases
Context Dependent Analysis of BioAmbients
No full textBioAmbients is a derivative of mobile ambients that has shown promise of describing interesting features of the behaviour of biological systems. The technical contribution of this paper is to extend the Flow Logic approach to static analysis with a couple of new techniques in order to give precise information about the behaviour of systems written in BioAmbients. Applying the development to a simple model of a cell releasing nutrients from food compunds we illustrate how the proposed analysis does indeed improve on previous efforts
Design, Analysis and Reasoning about Tools: Abstracts from the Third Workshop
No full texts from the Third Workshop Flemming Nielson (editor) October 1993 1 Introduction The third DART workshop took place on Thursday August l9th and Friday August 20th at the Department of Computer Science (DIKU) at the University of Copenhagen; it was organized by Mads Rosendahl and others at DIKU, and Torben Amtoft and Susanne Brønberg helped producing this report. The first day comprised survey presentations whereas the second contained more research oriented talks. The primary aim of the workshop was to increase the awareness of DART participants for each other's work, to stimulate collaboration between the di#erent groups, and to inform Danish industry about the skills possessed by the groups. The DART project started in March 1991 (prematurely terminating a smaller project on Formal Implementation, Transformation and Analysis of Programs) and is funded by the Danish Research Councils as part of the Danish Research Programme on Informatics. To date it has received about 8 million Danis..
Trust-Based Enforcement of Security Policies
No full textTwo conflicting high-level goals govern the enforcement of security policies, abridged in the phrase “high security at a low cost”. While these drivers seem irreconcilable, formal modelling languages and automated verification techniques can facilitate the task of finding the right balance. We propose a modelling language and a framework in which security checks can be relaxed or strengthened to save resources or increase protection, on the basis of trust relationships among communicating parties. Such relationships are automatically derived through a reputation system, hence adapt dynamically to the observed behaviour of the parties and are not fixed a priori. In order to evaluate the impact of the approach, we encode our modelling language in StoKlaim, which enables verification via the dedicated statistical model checker SAM. The overall approach is applied to a fragment of a Wireless Sensor Network, where there is a clear tension between devices with limited resources and the cost for securing the communication
Alternation-free Least Fixed Point Logic and it is implemented in SML
No full textAbstract. The Succinct Solver of Nielson and Seidl is based on th
Fitness Conditions for fixed Point Iteration
No full textThis paper provides a link between the formulation of static program analyses using the framework of abstract interpretation (popular for functional languages) and using the more classical framework of data flow analysis (popular for imperative languages). In particular we show how the classical notions of fastness, rapidity and k-boundedness carry over to the abstract interpretation framework and how this may be used to bound the number of times a functional should be unfolded in order to yield the fixed point. This is supplemented with a number of results on how to calculate the bounds for iterative forms (as for tail recursion), for linear forms (as for one nested recursive call), and for primitive recursive forms. In some cases this improves the ''worst case'' results of H.R. Nielson and F. Nielson: Bounded Fixed Point Iteration, but more importantly it gives much better ''average case'' results
Provably Correct Implementations of Services
No full textA number of formalisms have been defined to support the specification and analysis of service oriented applications. These formalisms have been equipped with tools (types or logics) to guarantee the correct behavior of the specified services. Due to the semantic gap between the specification formalism and the programming languages of service oriented overlay computers a critical issue is guaranteeing that correctness is preserved when running the specified systems over available implementations. We have defined a service oriented abstract machine, equipped with a formal structural semantics, that can be used to implement service specification formalisms. We use our abstract machine to implement different service oriented formalisms that have been recently proposed, each posing specific challenges that we can address successfully. By exploiting the SOS semantics of the abstract machine and those of the considered service oriented formalisms we do prove that our implementations are correct (sound and complete). We also discuss possible implementations of other formalisms
- …
