Digital Security (DiS) Research Publications

2015 2013 2012 2011 2010 2009 2008


Marko van Eekelen (editor), and Olha Shkaravska (editor). International Workshop on Foundational and Practical Aspects of Resource Analysis FOPARA . Technical report: ICIS-R09008, December, Radboud University Nijmegen, 2009.

The FOPARA workshop serves as a forum for presenting original research results that are relevant to the analysis of resource (time, space) consumption by computer programs. FOPARA aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions have been encouraged. The contributions cover the following topics: resource analysis for embedded systems, logical and machine-independent characterisations of complexity classes, logics closely related to complexity classes, type systems for controlling complexity, semantic methods to analyse resources, incl. quasi- and sup-interpretations, practical applications of resource analysis, etc. After the workshop the program committee will select papers for nal proceedings. These nal proceedings will be published by Springer in a volume of the Lecture Notes in Computer Science series.

[ PDF ] [ Bibtex ]

Christian Haack, and Erik Poll. Type-based Object Immutability with Flexible Initialization. Technical report: ICIS-R09001, January, Radboud University Nijmegen, 2009.

We present a type system for checking object immutability, reference immutability, and class immutability in an open or closed world. In order to separate object initialization from object constructors (which is often needed in practice), immutable objects are initialized in lexically scoped regions. The system is simple and direct; its only type qualifiers specify immutability properties. No auxiliary annotations, e.g., ownership types, are needed, yet good support for deep immutability is provided. To express object confinement, as required for class immutability in an open world, we make use of qualifier polymorphism. The system has two versions: one version with explicit specification commands that delimit the object initialization phase, and one version where such commands are implicit and inferred. In the latter version, all annotations are compatible with Java`s extended annotation syntax, as proposed in JSR 308.

[ PDF ] [ Bibtex ]

Wojciech Mostowski, and Erik Poll. Midlet Navigation Graphs in JML. Technical report: ICIS-R09004, August, Radboud University Nijmegen, 2009.

In the context of the Mobius project on Proof Carrying Code for mobile device Java applications (so called midlets), we present a way to formalise midlet navigation graphs in Java Modelling Language. Navigation graphs are used to express certain security policies of a midlet. Our resulting JML specifications are automatically verifiable with the static Java checker ESC/Java2. In the paper we relate to the earlier work on midlet navigation graphs generation from Java bytecode. Our work complements this earlier work by providing a mechanisms for establishing midlet navigation graph properties. In the paper we also discuss in detail practical difficulties with creating efficient and meaningful JML specifications for automatic verification with a lightweight verification tool. Our work was guided by one of the Mobius project realistically sized case studies developed by our industrial partners.

[ PDF ] [ Bibtex ]

O. Shkaravska, M. van Eekelen, and A. Tamalet. Collected Size Semantics for Functional Programs over Polymorphic Nested Lists. Technical report: ICIS-R09003, July, Radboud University Nijmegen, 2009.

Size analysis is an important prerequisite for heap consumption analysis. This paper is part of ongoing work about typing support for checking output-on-input size dependencies for function definitions in a strict functional language. A significant restriction for our earlier results is that emph{inner} data structures (e.g. in a list of lists) all must have the same size. Here, we make a big step forwards by overcoming this limitation via the introduction of higher-order size annotations such that variate sizes of inner data structures can be expressed.

[ PDF ] [ Bibtex ]