Search Results

Documents authored by Hansen, René Rydhof

Artifact
Software
DOI: 10.4230/artifacts.27330
LC4S-Rocq

Authors: Casper Ståhl, Levs Gondelman, René Rydhof Hansen, and Danny Bøgsted Poulsen

Abstract
Cite as

Casper Ståhl, Levs Gondelman, René Rydhof Hansen, Danny Bøgsted Poulsen. LC4S-Rocq (Software, Source code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27330,
   title = {{LC4S-Rocq}}, 
   author = {St\r{a}hl, Casper and Gondelman, Levs and Hansen, Ren\'{e} Rydhof and Poulsen, Danny B{\o}gsted},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:828cd84332eae467073735e4aee31198815adf58;origin=https://github.com/CasperStaahl/LC4S-Rocq;visit=swh:1:snp:6621719c2965396c06e9906088cd29f038a2d0fa;anchor=swh:1:rev:6fb8b0157f1fffd88ff7c55f72b2b19eb8c2e603}{\texttt{swh:1:dir:828cd84332eae467073735e4aee31198815adf58}} (visited on 2026-07-30)},
   url = {https://github.com/CasperStaahl/LC4S-Rocq},
   doi = {10.4230/artifacts.27330},
}
Document
DOI: 10.4230/LIPIcs.TYPES.2025.6
Formalisation and Extension of Lagois Connections for Secure Information Flow

Authors: Casper Ståhl, Levs Gondelman, René Rydhof Hansen, and Danny Bøgsted Poulsen

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

Abstract
Lagois connections have been proposed as a way to formulate and formalise a secure information flow policy between two organisations each with their own information flow policies that must also be enforced. By composing Lagois connections in a chain, it is possible to compose the information flow policies of several organisations. However, chains are not always suitable. For example, if one of the "links" in the chain enforces a coarser policy than the surrounding links, this corresponds to taking low security information as input and reclassifying it as high security, preventing further communication of (formerly low) information at the low security level. This is an instance of the well-known problem of "label creep". In this paper we extend the compositionality results of Lagois connections to forests, and graphs that "behave" like forests, of Lagois connections. In addition to the extra flexibility gained in the communication topology, it also solves the label creep problem: Intuitively, to bypass the problematic intermediary, we can verify that the subgraph bypassing the problematic intermediary is located in a forest of secure sub-graphs. We show that this is sound with respect to noninterference, by proving that if information in a program flows according to a secure graph then an attacker can never observe a policy violation in the system. As a further contribution of this paper, all of the above has been formalised in the Rocq proof assistant, including a novel formalisation of a substantial part of the literature of Lagois connections, providing a strong foundation for future work and implementations.
Cite as

Casper Ståhl, Levs Gondelman, René Rydhof Hansen, and Danny Bøgsted Poulsen. Formalisation and Extension of Lagois Connections for Secure Information Flow. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{stahl_et_al:LIPIcs.TYPES.2025.6,
  author =	{St\r{a}hl, Casper and Gondelman, Levs and Hansen, Ren\'{e} Rydhof and Poulsen, Danny B{\o}gsted},
  title =	{{Formalisation and Extension of Lagois Connections for Secure Information Flow}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.6},
  URN =		{urn:nbn:de:0030-drops-270247},
  doi =		{10.4230/LIPIcs.TYPES.2025.6},
  annote =	{Keywords: Lagois connection, information flow, security}
}
Document
DOI: 10.4230/OASIcs.SSV.2011.32
Adaptable Value-Set Analysis for Low-Level Code

Authors: Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)

Abstract
This paper presents a framework for binary code analysis that uses only SAT-based algorithms. Within the framework, incremental SAT solving is used to perform a form of weakly relational value-set analysis in a novel way, connecting the expressiveness of the value sets to computational complexity. Another key feature of our framework is that it translates the semantics of binary code into an intermediate representation. This allows for a straightforward translation of the program semantics into Boolean logic and eases the implementation efforts, too. We show that leveraging the efficiency of contemporary SAT solvers allows us to prove interesting properties about medium-sized microcontroller programs.
Cite as

Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen. Adaptable Value-Set Analysis for Low-Level Code. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 32-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{brauer_et_al:OASIcs.SSV.2011.32,
  author =	{Brauer, J\"{o}rg and Hansen, Ren\'{e} Rydhof and Kowalewski, Stefan and Larsen, Kim G. and Olesen, Mads Chr.},
  title =	{{Adaptable Value-Set Analysis for Low-Level Code}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{32--43},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{Brauer, J\"{o}rg and Roveri, Marco and Tews, Hendrik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.32},
  URN =		{urn:nbn:de:0030-drops-35884},
  doi =		{10.4230/OASIcs.SSV.2011.32},
  annote =	{Keywords: Abstract interpretation, SAT solving, embedded systems}
}
Document
DOI: 10.4230/OASIcs.WCET.2012.1
What is a Timing Anomaly?

Authors: Franck Cassez, René Rydhof Hansen, and Mads Chr. Olesen

Published in: OASIcs, Volume 23, 12th International Workshop on Worst-Case Execution Time Analysis (2012)

Abstract
Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.
Cite as

Franck Cassez, René Rydhof Hansen, and Mads Chr. Olesen. What is a Timing Anomaly?. In 12th International Workshop on Worst-Case Execution Time Analysis. Open Access Series in Informatics (OASIcs), Volume 23, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{cassez_et_al:OASIcs.WCET.2012.1,
  author =	{Cassez, Franck and Hansen, Ren\'{e} Rydhof and Olesen, Mads Chr.},
  title =	{{What is a Timing Anomaly?}},
  booktitle =	{12th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{1--12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-41-5},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{23},
  editor =	{Vardanega, Tullio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2012.1},
  URN =		{urn:nbn:de:0030-drops-35521},
  doi =		{10.4230/OASIcs.WCET.2012.1},
  annote =	{Keywords: Timing anomalies, worst case execution time (WCET), abstractions}
}
Document
DOI: 10.4230/OASIcs.WCET.2010.113
METAMOC: Modular Execution Time Analysis using Model Checking

Authors: Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, and Kim Guldstrand Larsen

Published in: OASIcs, Volume 15, 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)

Abstract
Safe and tight worst-case execution times (WCETs) are important when scheduling hard real-time systems. This paper presents METAMOC, a modular method, based on model checking and static analysis, that determines safe and tight WCETs for programs running on platforms featuring caching and pipelining. The method works by constructing a UPPAAL model of the program being analysed and annotating the model with information from an inter-procedural value analysis. The program model is then combined with a model of the hardware platform and model checked for the WCET. Through support for the platforms ARM7, ARM9 and ATMEL AVR 8-bit, the modularity and retargetability of the method are demonstrated, as only the pipeline needs to be remodelled. Hardware modelling is performed in a state-of-the-art graphical modelling environment. Experiments on the Mälardalen WCET benchmark programs show that taking caching into account yields much tighter WCETs than without modelling caches, and that METAMOC is a sufficiently fast and versatile approach for WCET analysis.
Cite as

Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, and Kim Guldstrand Larsen. METAMOC: Modular Execution Time Analysis using Model Checking. In 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010). Open Access Series in Informatics (OASIcs), Volume 15, pp. 113-123, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{dalsgaard_et_al:OASIcs.WCET.2010.113,
  author =	{Dalsgaard, Andreas E. and Olesen, Mads Chr. and Toft, Martin and Hansen, Ren\'{e} Rydhof and Larsen, Kim Guldstrand},
  title =	{{METAMOC: Modular Execution Time Analysis using Model Checking}},
  booktitle =	{10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)},
  pages =	{113--123},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-21-7},
  ISSN =	{2190-6807},
  year =	{2010},
  volume =	{15},
  editor =	{Lisper, Bj\"{o}rn},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2010.113},
  URN =		{urn:nbn:de:0030-drops-28319},
  doi =		{10.4230/OASIcs.WCET.2010.113},
  annote =	{Keywords: WCET analysis, timed automata, model checking, UPPAAL}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact