Digital Security (DiS) Research Publications


2015 2013 2012 2011 2010 2009 2008

Journal

David Galindo, Paz Morillo, and Carla Rífols. Improved certificate-based encryption in the standard model. In: Journal of Systems and Software, Nr: 7, Vol: 81, Pages: 1218-1226, Elsevier, 2008.

[ External URL ] [ Bibtex ]

Wolter Pieters, and Robert van Haren. Temptations of turnout and modernisation: e-voting discourses in the UK and the Netherlands. In: Journal of Information, Communication and Ethics in Society, Nr: 4, Vol: 5, Pages: 276-292, 2008.

[ Missing PDF ] [ Bibtex ]

Conference

Andr\ and P. R. D`Argenio. Significant Diagnostic Counterexamples in Probabilistic Model Checking. In: Haifa Verification Conference: 4th International Conference (HVC 08), Lect. Notes Comp. Sci., Vol: 5394, Pages: 129-148, 2008.

[ Missing PDF ] [ Bibtex ]

Miguel E. Andr\'es. Conditional Probabilities over Probabilistic and Nondeterministic Systems. In: Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference (TACAS , Lect. Notes Comp. Sci., Vol: 4963, Pages: 157-172, 2008.

[ Missing PDF ] [ Bibtex ]

Marko van Eekelen, Stefan ten Hoedt, Rene Schreurs, and Yaroslav Usenko. Analysis of a Session-Layer Protocol in mCRL2. Verification of a Real-Life Industrial Implementation. In: Proc. 12th Int. Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007), Edited by: P. Merino, and S. Leue. Lect. Notes Comp. Sci., Vol: 4916, Pages: 182-199, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

AHA: Amortized Heap Space Usage Analysis. In: Trends in Functional Programming Volume 8: Selected Papers of the $8^{th}$ International Symposium on Trends in Functional Programming (TFP, Pages: 36-53, 2008.

[ Missing PDF ] [ Bibtex ]

Leonard Lensink, Sjaak Smetsers, and Marko van Eekelen. Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization. In: Proc. 12th Int. Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007), Edited by: P. Merino, and S. Leue. Lect. Notes Comp. Sci., Vol: 4916, Pages: 115-132, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Maarten de Mol, Marko van Eekelen, and Rinus Plasmeijer. Proving Properties of Lazy Functional Programs with SPARKLE. In: 2nd Central-European Functional Programming School, CEFP 2007, Edited by: Zolt\'an Horv\'ath. Lect. Notes Comp. Sci. # " Tutorial Series", Vol: 5161, Pages: 41-86, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Maarten de Mol, Marko van Eekelen, and Rinus Plasmeijer. A Single-Step Term-Graph Reduction System for Proof Assistants. In: Applications of Graph Transformations with Industrial Relevance, Third International Symposium, AGTIVE 2007. Proceedings of Selected and Invited Papers, Edited by: Sch\. Lect. Notes Comp. Sci., Vol: 5088, Pages: 184-200, October, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Reports

Peter Achten, Marko van Eekelen, Maarten de Mol, and Rinus Plasmeijer. A Common Arrow Based Semantics for GEC and iData Applications. Technical report: ICIS-R08023, December, Radboud University Nijmegen, 2008.

State-based interactive applications, whether they run on the desktop or as a web application, can be considered as collections of interconnected editors of structured values that allow users to manipulate data. This is the view that is advocated by the GEC and iData toolkits, which offer a high level of abstraction to programming desktop and web GUI applications respectively. Special features of these toolkits are that editors have shared, persistent state, and that they handle events individually. In this paper we cast these toolkits within the Arrow framework and present a single, uni¯ed semantic model that defines shared state and event handling. We study the properties of this EditorArrow model, and of editors in particular. Furthermore, we present the definedness properties of the combinators. A reference implementation of the EditorArrow model is given with some small program examples. We discuss formal reasoning about the model using the proof assistant Sparkle.

[ PDF ] [ Bibtex ]

Luc Rutten, and M.C.J.D. van Eekelen. Efficient and Formally Proven Reduction of Large Integers by Small Moduli. Technical report: ICIS-R08001, February, Radboud University Nijmegen, 2008.

On $w$-bit processors which are much faster at multiplying two $w$-bit integers than at dividing $2w$-bit integers by $w$-bit integers, reductions of large integers by moduli $M$ smaller than $2^{w-1}$ are often implemented sub-optimally, leading applications to take excessive processing time. We present a modular reduction algorithm implementing division by a modulus through multiplication by a reciprocal of that modulus, a well-known method for moduli larger than $2^{w-1}$. We show that application of this method to smaller moduli makes it possible to express certain modular sums and differences without having to compensate for word overflows. By embedding the algorithm in a loop and applying a few transformations to the loop, we obtain an algorithm for reduction of large integers by moduli up to $2^{w-1}$. Implementations of this algorithm can run considerably faster than implementations of similar algorithms that allow for moduli up to $2^w$. This is substantiated by measurements on processors with relatively fast multiplication instructions. It is notoriously hard to specify efficient mathematical algorithms on the level of abstract machine instructions in an error-free manner. In order to eliminate the chance of errors as much as possible, we have created formal correctness proofs of our algorithms, checked by a mechanized proof assistant.

[ PDF ] [ Bibtex ]

Bernard van Gastel, Leonard Lensink, Sjaak Smetsers, and M.C.J.D. van Eekelen. Reentrant Readers-Writers: A Case Study Combining Model Checking and Theorem Proving. Technical report: ICIS-R08005, April, Radboud University Nijmegen, 2008.

The classic readers-writers problem has been extensively studied. This holds to a lesser degree for the reentrant version, where it is allowed to nest locking actions. Such nesting is useful when a library is created with various procedures that each start and end with a lock. Allowing nesting makes it possible for these procedures to call each other. We considered an existing widely used industrial implementation of the reentrant readers-writers problem. We modeled it using a model checker revealing a serious error: a possible deadlock situation. The model was improved and checked satisfactorily for a fixed number of processes. To achieve a correctness result for an arbitrary number of processes the model was converted to a theorem prover with which it was proven.

[ PDF ] [ Bibtex ]

Christian Haack, Marieke Huisman, and Clement Hurlin. Reasoning about Java`s Reentrant Locks. Technical report: ICIS-R08014, July, Radboud University Nijmegen, 2008.

This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each lock is associated with a resource invariant, when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parametrized classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.

[ PDF ] [ Bibtex ]

Marieke Huisman, and Erik Poll. Formal Techniques for Java-like Pograms (FTfJP08). Technical report: ICIS-R08013, June, Radboud University Nijmegen, 2008.

This report contains the papers presented at FTfJP`08: the 10th workshop on Formal Techniques for Java-like Programs held on July 8th, 2008 in Paphos, Cyprus. This workshop is the tenth in a series of workshops aimed at applying formal techniques to improve modern object-oriented languages. Newer languages such as Java and C# provide good platforms to bridge the gap between formal techniques and practical program development, because of their reasonably clear semantics and standardized libraries. It is our hope that this workshop will encourage the further deployment of well-considered formal techniques.

[ PDF ] [ Bibtex ]

Rinus Plasmeijer, Sjaak Smetsers, and Arjen van Weelden. Interactive Combining of Typed Object Code. Technical report: ICIS-R08019, November, Radboud University Nijmegen, 2008.

The functional language Clean includes a hybrid type system: in addition to the traditional static type system it offers support for dynamically typed values, so called \emph{dynamics}. An expression of arbitrary static type can be packed into a dynamic, and via pattern matching on types a dynamic can be converted back to a value of statically known type. The most important aspect of dynamics is that they can be serialized, written to file, and exchanged between independently compiled applications in a type-safe way. Since dynamics may contain functions and closures, they can be regarded as type-safe plugins. An application can combine plugins in a type safe way to new ones, without having to know what the actual contents and types of the original plugins are. In this paper we explain the underlying implementation and the architecture of the run-time system needed to make this all possible. To show the expressive power of Clean`s dynamics we present an interactive shell, called Esther. The command line language of this shell provides the basic functionality of a strongly typed lazy functional language. Esther behaves like an interpreter (direct response) yet its resulting performance is comparable to compiled code. This is achieved by using the dynamic facility of Clean. The shell actually combines compiled code; no help from a compiler is needed. Moreover, type checking is for free using the run-time type unification of dynamics. In this way we have obtained a novel architectural framework in which one can freely mix functionality created by the compiler, functionality stored in dynamics by compiled applications, and functionality interactively created by using the shell command line interpreter.

[ PDF ] [ Bibtex ]

O. Shkaravska, M. van Eekelen, and A. Tamalet. Collected Size Semantics for Functional Programs over Lists. Technical report: ICIS-R08021, November, 2008.

This work introduces collected size semantics of strict functional programs over lists. The collected size semantics of a function definition is a multivalued size function that collects the dependencies between every possible output size and the corresponding input sizes. Such functions annotate standard types and are defined by conditional rewriting rules generated during type inference. We focus on the connection between the rewriting rules and lower and upper bounds on the multivalued size functions, when the bounds are given by piecewise polynomials. We show how, given a set of conditional rewriting rules, one can infer bounds that define an indexed family of polynomials that approximates the multivalued size function. Using collected size semantics we are able to infer non-monotonic and non-linear lower and upper polynomial bounds for many functional programs. As a feasibility study, we use the procedure to infer lower and upper polynomial size-bounds on typical functions of a list library.

[ PDF ] [ Bibtex ]

O. Shkaravska, M. van Eekelen, and A. Tamalet. Polynomial Size Complexity Analysis with Families of Piecewise Polynomials (with soundness proof and examples in detail). Technical report: ICIS-R08020, November, Radboud University Nijmegen, 2008.

Size analysis can play an important role in optimising memory management and in preventing failure due to memory exhaustion. Static size analysis can be performed using size-aware type systems. In size-aware type systems types express output-on-input size dependencies where sizes of outputs depend on sizes of inputs but they do not depend directly on the actual values. We present a novel type system for a strict functional language. We introduce size annotations that are indexed families of piecewise polynomials. Families are de?ned using indices. They collect possible different size dependencies of a single function. With families compositionality becomes straightforward, even for non-monotonic size dependencies. Lower and upper size bounds can be expressed in a natural way as members of the family. Furthermore, families make it possible to allow non matrix-like structures where inner lists have different lengths. The type system is proven to be sound with respect to a standard operational semantics. Type checking in our type system is not fully decidable. However, we identify two large decidable subclasses. Moreover, the type system admits a semi-automatic inference procedure.

[ PDF ] [ Bibtex ]

Sjaak Smetsers, and Erik Barendsen. Formalizing Type Theory in PVS: a case study. Technical report: ICIS-R08022, December, Radboud University Nijmegen, 2008.

In this case study we investigate the use of PVS for developing type theoretical concepts and verifying the correctness of a typing algorithm. PVS turns out to be very useful for efficient development of a sound basic theory about polymorphic typing. This research contributes to the PoplMark challenge on mechanizing metatheory

[ PDF ] [ Bibtex ]

Alejandro Tamalet, Olha Shkaravska, and Marko van Eekelen. A Size-Aware Type System with Algebraic Data Types. Technical report: ICIS-R08006, April, Radboud University Nijmegen, 2008.

We present a size-aware type system for a first-order functional language with algebraic data types, where types are annotated with polynomials over size variables. We define how to generate typing rules for each data type, provided its user defined size function meets certain requirements. As an example, a program for balancing binary trees is type checked. The type system is shown to be sound with respect to the operational semantics in the class of shapely functions. Type checking is shown to be undecidable, however, decidability for a large subset of programs is guaranteed.

[ PDF ] [ Bibtex ]

Hendrik Tews, Tjark Weber, Marcus Völp, Erik Poll, M.C.J.D. van Eekelen, and Peter van Rossum. Nova Micro-Hypervisor Verification. Technical report: ICIS-R08012, May, Radboud University Nijmegen, 2008, Robin deliverable D13.

In this document we describe the work performed in the Robin project towards verifying the Nova micro-hypervisor operating-system kernel. In particular, we describe in detail the Robin verification environment and the results obtained with it. The Robin verification environment consists of the interactive theorem prover PVS, an IA32 (x86) hardware model in PVS, a semantics of (a rich subset of) C++, and a semantics compiler translating C++ sources into their semantics in PVS.

[ PDF ] [ Bibtex ]

H. Tews, Tjark Weber, E. Poll, and M.C.J.D. van Eekelen. Formal Nova interface specification. Technical report: ICIS-R08011, May, 2008, Robin deliverable D12.

This document contains one major result of work package 4 (kernel specification and verification): a formal specification of the Nova interface. The specification consists of three main parts: (1) a definition of an abstract internal state for the Nova micro-hypervisor, (2) a description of the operations of the hypervisor in imperative pseudo-code that accesses and modifies the internal state, and (3) a combination of big-step denotational and small-step operational semantics to give semantics to the pseudo code as state modifying functions.

[ PDF ] [ Bibtex ]