Showing 1–15 of 15 results for author: König, J

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)

Authors: Linard Arquint, Samarth Kishor, Jason R. Koenig, Joey Dodds, Daniel Kroening, Peter Müller

Abstract: Existing program verifiers can prove advanced properties about security protocol implementations, but are difficult to scale to large codebases because of the manual effort required. We develop a novel methodology called *Diodon* that addresses this challenge by splitting the codebase into the protocol implementation (the *Core*) and the remainder (the *Application*). This split allows us to apply… ▽ More Existing program verifiers can prove advanced properties about security protocol implementations, but are difficult to scale to large codebases because of the manual effort required. We develop a novel methodology called *Diodon* that addresses this challenge by splitting the codebase into the protocol implementation (the *Core*) and the remainder (the *Application*). This split allows us to apply powerful semi-automated verification techniques to the security-critical Core, while fully-automatic static analyses scale the verification to the entire codebase by ensuring that the Application cannot invalidate the security properties proved for the Core. The static analyses achieve that by proving *I/O independence*, i.e., that the I/O operations within the Application are independent of the Core's security-relevant data (such as keys), and that the Application meets the Core's requirements. We have proved Diodon sound by first showing that we can safely allow the Application to perform I/O independent of the security protocol, and second that manual verification and static analyses soundly compose. We evaluate Diodon on two case studies: an implementation of the signed Diffie-Hellman key exchange and a large (100k+ LoC) production Go codebase implementing a key exchange protocol for which we obtained secrecy and injective agreement guarantees by verifying a Core of about 1% of the code with the auto-active program verifier Gobra in less than three person months. △ Less

Submitted 1 July, 2025; originally announced July 2025.

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules (Technical Report)

Authors: Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao

Abstract: Verified compilation of open modules (i.e., modules whose functionality depends on other modules) provides a foundation for end-to-end verification of modular programs ubiquitous in contemporary software. However, despite intensive investigation in this topic for decades, the proposed approaches are still difficult to use in practice as they rely on assumptions about the internal working of compil… ▽ More Verified compilation of open modules (i.e., modules whose functionality depends on other modules) provides a foundation for end-to-end verification of modular programs ubiquitous in contemporary software. However, despite intensive investigation in this topic for decades, the proposed approaches are still difficult to use in practice as they rely on assumptions about the internal working of compilers which make it difficult for external users to apply the verification results. We propose an approach to verified compositional compilation without such assumptions in the setting of verifying compilation of heterogeneous modules written in first-order languages supporting global memory and pointers. Our approach is based on the memory model of CompCert and a new discovery that a Kripke relation with a notion of memory protection can serve as a uniform and composable semantic interface for the compiler passes. By absorbing the rely-guarantee conditions on memory evolution for all compiler passes into this Kripke Memory Relation and by piggybacking requirements on compiler optimizations onto it, we get compositional correctness theorems for realistic optimizing compilers as refinements that directly relate native semantics of open modules and that are ignorant of intermediate compilation processes. Such direct refinements support all the compositionality and adequacy properties essential for verified compilation of open modules. We have applied this approach to the full compilation chain of CompCert with its Clight source language and demonstrated that our compiler correctness theorem is open to composition and intuitive to use with reduced verification complexity through end-to-end verification of non-trivial heterogeneous modules that may freely invoke each other (e.g., mutually recursively). △ Less

Submitted 18 November, 2023; v1 submitted 25 February, 2023; originally announced February 2023.

AuthentiSense: A Scalable Behavioral Biometrics Authentication Scheme using Few-Shot Learning for Mobile Platforms

Authors: Hossein Fereidooni, Jan König, Phillip Rieger, Marco Chilese, Bora Gökbakan, Moritz Finke, Alexandra Dmitrienko, Ahmad-Reza Sadeghi

Abstract: Mobile applications are widely used for online services sharing a large amount of personal data online. One-time authentication techniques such as passwords and physiological biometrics (e.g., fingerprint, face, and iris) have their own advantages but also disadvantages since they can be stolen or emulated, and do not prevent access to the underlying device, once it is unlocked. To address these c… ▽ More Mobile applications are widely used for online services sharing a large amount of personal data online. One-time authentication techniques such as passwords and physiological biometrics (e.g., fingerprint, face, and iris) have their own advantages but also disadvantages since they can be stolen or emulated, and do not prevent access to the underlying device, once it is unlocked. To address these challenges, complementary authentication systems based on behavioural biometrics have emerged. The goal is to continuously profile users based on their interaction with the mobile device. However, existing behavioural authentication schemes are not (i) user-agnostic meaning that they cannot dynamically handle changes in the user-base without model re-training, or (ii) do not scale well to authenticate millions of users. In this paper, we present AuthentiSense, a user-agnostic, scalable, and efficient behavioural biometrics authentication system that enables continuous authentication and utilizes only motion patterns (i.e., accelerometer, gyroscope and magnetometer data) while users interact with mobile apps. Our approach requires neither manually engineered features nor a significant amount of data for model training. We leverage a few-shot learning technique, called Siamese network, to authenticate users at a large scale. We perform a systematic measurement study and report the impact of the parameters such as interaction time needed for authentication and n-shot verification (comparison with enrollment samples) at the recognition stage. Remarkably, AuthentiSense achieves high accuracy of up to 97% in terms of F1-score even when evaluated in a few-shot fashion that requires only a few behaviour samples per user (3 shots). Our approach accurately authenticates users only after 1 second of user interaction. For AuthentiSense, we report a FAR and FRR of 0.023 and 0.057, respectively. △ Less

Submitted 6 February, 2023; originally announced February 2023.

Comments: 16 pages, 7 figures

Grounding Game Semantics in Categorical Algebra

Authors: Jérémie Koenig

Abstract: I present a formal connection between algebraic effects and game semantics, two important lines of work in programming languages semantics with applications in compositional software verification. Specifically, the algebraic signature enumerating the possible side-effects of a computation can be read as a game, and strategies for this game constitute the free algebra for the signature in a cate… ▽ More I present a formal connection between algebraic effects and game semantics, two important lines of work in programming languages semantics with applications in compositional software verification. Specifically, the algebraic signature enumerating the possible side-effects of a computation can be read as a game, and strategies for this game constitute the free algebra for the signature in a category of complete partial orders (cpos). Hence, strategies provide a convenient model of computations with uninterpreted side-effects. In particular, the operational flavor of game semantics carries over to the algebraic context, in the form of the coincidence between the initial algebras and the terminal coalgebras of cpo endofunctors. Conversely, the algebraic point of view sheds new light on the strategy constructions underlying game semantics. Strategy models can be reformulated as ideal completions of partial strategy trees (free dcpos on the term algebra). Extending the framework to multi-sorted signatures would make this construction available for a large class of games. △ Less

Submitted 3 November, 2022; originally announced November 2022.

Comments: In Proceedings ACT 2021, arXiv:2211.01102

ACM Class: D.3.1; F.3.2

Journal ref: EPTCS 372, 2022, pp. 368-383

What's Cracking? A Review and Analysis of Deep Learning Methods for Structural Crack Segmentation, Detection and Quantification

Authors: Jacob König, Mark Jenkins, Mike Mannion, Peter Barrie, Gordon Morison

Abstract: Surface cracks are a very common indicator of potential structural faults. Their early detection and monitoring is an important factor in structural health monitoring. Left untreated, they can grow in size over time and require expensive repairs or maintenance. With recent advances in computer vision and deep learning algorithms, the automatic detection and segmentation of cracks for this monitori… ▽ More Surface cracks are a very common indicator of potential structural faults. Their early detection and monitoring is an important factor in structural health monitoring. Left untreated, they can grow in size over time and require expensive repairs or maintenance. With recent advances in computer vision and deep learning algorithms, the automatic detection and segmentation of cracks for this monitoring process have become a major topic of interest. This review aims to give researchers an overview of the published work within the field of crack analysis algorithms that make use of deep learning. It outlines the various tasks that are solved through applying computer vision algorithms to surface cracks in a structural health monitoring setting and also provides in-depth reviews of recent fully, semi and unsupervised approaches that perform crack classification, detection, segmentation and quantification. Additionally, this review also highlights popular datasets used for cracks and the metrics that are used to evaluate the performance of those algorithms. Finally, potential research gaps are outlined and further research directions are provided. △ Less

Submitted 8 February, 2022; originally announced February 2022.

Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion

Authors: Jason R. Koenig, Oded Padon, Sharon Shoham, Alex Aiken

Abstract: We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new syntactic form for quantifier-free bodies. The breadth-first strategy prevents inductive generalization from getting stuck in regions of the search space th… ▽ More We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new syntactic form for quantifier-free bodies. The breadth-first strategy prevents inductive generalization from getting stuck in regions of the search space that are expensive to search and focuses instead on lemmas that are easy to discover. The new syntactic form is well-suited to lemmas with quantifier alternations by allowing both limited conjunction and disjunction in the quantifier-free body, while carefully controlling the size of the search space. Combining the breadth-first strategy with the new syntactic form results in useful inductive bias by prioritizing lemmas according to: (i) well-defined syntactic metrics for simple quantifier structures and quantifier-free bodies, and (ii) the empirically useful heuristic of preferring lemmas that are fast to discover. On a benchmark suite of primarily distributed protocols and complex Paxos variants, we demonstrate that our algorithm can solve more of the most complicated examples than state-of-the-art techniques. △ Less

Submitted 9 December, 2021; originally announced December 2021.

Comments: 16 pages, 2 figures, submitted to TACAS 2022

ACM Class: D.2.4; F.3.1

Weakly-Supervised Surface Crack Segmentation by Generating Pseudo-Labels using Localization with a Classifier and Thresholding

Authors: Jacob König, Mark Jenkins, Mike Mannion, Peter Barrie, Gordon Morison

Abstract: Surface cracks are a common sight on public infrastructure nowadays. Recent work has been addressing this problem by supporting structural maintenance measures using machine learning methods. Those methods are used to segment surface cracks from their background, making them easier to localize. However, a common issue is that to create a well-functioning algorithm, the training data needs to have… ▽ More Surface cracks are a common sight on public infrastructure nowadays. Recent work has been addressing this problem by supporting structural maintenance measures using machine learning methods. Those methods are used to segment surface cracks from their background, making them easier to localize. However, a common issue is that to create a well-functioning algorithm, the training data needs to have detailed annotations of pixels that belong to cracks. Our work proposes a weakly supervised approach that leverages a CNN classifier in a novel way to create surface crack pseudo labels. First, we use the classifier to create a rough crack localization map by using its class activation maps and a patch based classification approach and fuse this with a thresholding based approach to segment the mostly darker crack pixels. The classifier assists in suppressing noise from the background regions, which commonly are incorrectly highlighted as cracks by standard thresholding methods. Then, the pseudo labels can be used in an end-to-end approach when training a standard CNN for surface crack segmentation. Our method is shown to yield sufficiently accurate pseudo labels. Those labels, incorporated into segmentation CNN training using multiple recent crack segmentation architectures, achieve comparable performance to fully supervised methods on four popular crack segmentation datasets. △ Less

Submitted 27 October, 2021; v1 submitted 1 September, 2021; originally announced September 2021.

Comments: This work has been submitted to the IEEE for possible publication

"Look! It's a Computer Program! It's an Algorithm! It's AI!": Does Terminology Affect Human Perceptions and Evaluations of Algorithmic Decision-Making Systems?

Authors: Markus Langer, Tim Hunsicker, Tina Feldkamp, Cornelius J. König, Nina Grgić-Hlača

Abstract: In the media, in policy-making, but also in research articles, algorithmic decision-making (ADM) systems are referred to as algorithms, artificial intelligence, and computer programs, amongst other terms. We hypothesize that such terminological differences can affect people's perceptions of properties of ADM systems, people's evaluations of systems in application contexts, and the replicability of… ▽ More In the media, in policy-making, but also in research articles, algorithmic decision-making (ADM) systems are referred to as algorithms, artificial intelligence, and computer programs, amongst other terms. We hypothesize that such terminological differences can affect people's perceptions of properties of ADM systems, people's evaluations of systems in application contexts, and the replicability of research as findings may be influenced by terminological differences. In two studies (N = 397, N = 622), we show that terminology does indeed affect laypeople's perceptions of system properties (e.g., perceived complexity) and evaluations of systems (e.g., trust). Our findings highlight the need to be mindful when choosing terms to describe ADM systems, because terminology can have unintended consequences, and may impact the robustness and replicability of HCI research. Additionally, our findings indicate that terminology can be used strategically (e.g., in communication about ADM systems) to influence people's perceptions and evaluations of these systems. △ Less

Submitted 26 May, 2022; v1 submitted 25 August, 2021; originally announced August 2021.

Comments: Preregistrations for the studies included in this paper are available under https://aspredicted.org/LDC\_GSM and https://aspredicted.org/NTE\_WND

Journal ref: In Proceedings of the 2022 CHI Conference on Human Factors in Computing Systems

Optimized Deep Encoder-Decoder Methods for Crack Segmentation

Authors: Jacob König, Mark Jenkins, Mike Mannion, Peter Barrie, Gordon Morison

Abstract: Surface crack segmentation poses a challenging computer vision task as background, shape, colour and size of cracks vary. In this work we propose optimized deep encoder-decoder methods consisting of a combination of techniques which yield an increase in crack segmentation performance. Specifically we propose a decoder-part for an encoder-decoder based deep learning architecture for semantic segmen… ▽ More Surface crack segmentation poses a challenging computer vision task as background, shape, colour and size of cracks vary. In this work we propose optimized deep encoder-decoder methods consisting of a combination of techniques which yield an increase in crack segmentation performance. Specifically we propose a decoder-part for an encoder-decoder based deep learning architecture for semantic segmentation and study its components to achieve increased performance. We also examine the use of different encoder strategies and introduce a data augmentation policy to increase the amount of available training data. The performance evaluation of our method is carried out on four publicly available crack segmentation datasets. Additionally, we introduce two techniques into the field of surface crack segmentation, previously not used there: Generating results using test-time-augmentation and performing a statistical result analysis over multiple training runs. The former approach generally yields increased performance results, whereas the latter allows for more reproducible and better representability of a methods results. Using those aforementioned strategies with our proposed encoder-decoder architecture we are able to achieve new state of the art results in all datasets. △ Less

Submitted 26 August, 2021; v1 submitted 14 August, 2020; originally announced August 2020.

Comments: Accepted Manuscript at Digital Signal Processing (Elsevier)

Multi-Stage Reinforcement Learning For Object Detection

Authors: Jonas Koenig, Simon Malberg, Martin Martens, Sebastian Niehaus, Artus Krohn-Grimberghe, Arunselvan Ramaswamy

Abstract: We present a reinforcement learning approach for detecting objects within an image. Our approach performs a step-wise deformation of a bounding box with the goal of tightly framing the object. It uses a hierarchical tree-like representation of predefined region candidates, which the agent can zoom in on. This reduces the number of region candidates that must be evaluated so that the agent can affo… ▽ More We present a reinforcement learning approach for detecting objects within an image. Our approach performs a step-wise deformation of a bounding box with the goal of tightly framing the object. It uses a hierarchical tree-like representation of predefined region candidates, which the agent can zoom in on. This reduces the number of region candidates that must be evaluated so that the agent can afford to compute new feature maps before each step to enhance detection quality. We compare an approach that is based purely on zoom actions with one that is extended by a second refinement stage to fine-tune the bounding box after each zoom step. We also improve the fitting ability by allowing for different aspect ratios of the bounding box. Finally, we propose different reward functions to lead to a better guidance of the agent while following its search trajectories. Experiments indicate that each of these extensions leads to more correct detections. The best performing approach comprises a zoom stage and a refinement stage, uses aspect-ratio modifying actions and is trained using a combination of three different reward metrics. △ Less

Submitted 26 October, 2018; v1 submitted 15 October, 2018; originally announced October 2018.

Comments: Accepted for the Computer Vision Conference (CVC) 2019

Some complexity and approximation results for coupled-tasks scheduling problem according to topology

Authors: Benoit Darties, Rodolphe Giroudeau, Jean-Claude König, Gilles Simonin

Abstract: We consider the makespan minimization coupled-tasks problem in presence of compatibility constraints with a specified topology. In particular, we focus on stretched coupled-tasks, i.e. coupled-tasks having the same sub-tasks execution time and idle time duration. We study several problems in framework of classic complexity and approximation for which the compatibility graph is bipartite (star, cha… ▽ More We consider the makespan minimization coupled-tasks problem in presence of compatibility constraints with a specified topology. In particular, we focus on stretched coupled-tasks, i.e. coupled-tasks having the same sub-tasks execution time and idle time duration. We study several problems in framework of classic complexity and approximation for which the compatibility graph is bipartite (star, chain,. . .). In such a context, we design some efficient polynomial-time approximation algorithms for an intractable scheduling problem according to some parameters. △ Less

Submitted 7 June, 2017; originally announced June 2017.

Journal ref: RAIRO - Operations Research, EDP Sciences, 2016, 50, pp.781 - 795

Isomorphic coupled-task scheduling problem with compatibility constraints on a single processor

Authors: Gilles Simonin, Benoit Darties, Rodolphe Giroudeau, Jean-Claude König

Abstract: The problem presented in this paper is a generalization of the usual coupled-tasks scheduling problem in presence of compatibility constraints. The reason behind this study is the data acquisition problem for a submarine torpedo. We investigate a particular configuration for coupled tasks (any task is divided into two sub-tasks separated by an idle time), in which the idle time of a coupled task i… ▽ More The problem presented in this paper is a generalization of the usual coupled-tasks scheduling problem in presence of compatibility constraints. The reason behind this study is the data acquisition problem for a submarine torpedo. We investigate a particular configuration for coupled tasks (any task is divided into two sub-tasks separated by an idle time), in which the idle time of a coupled task is equal to the sum of durations of its two sub-tasks. We prove -completeness of the minimization of the schedule length, we show that finding a solution to our problem amounts to solving a graph problem, which in itself is close to the minimum-disjoint-path cover (min-DCP) problem. We design a (3a+2b)/(2a+2b)-approximation, where a and b (the processing time of the two sub-tasks) are two input data such as a>b>0, and that leads to a ratio between 3/2 and 5/4. Using a polynomial-time algorithm developed for some class of graph of min-DCP, we show that the ratio decreases to 1.37 . △ Less

Submitted 7 June, 2017; originally announced June 2017.

Journal ref: Journal of Scheduling, Springer Verlag, 2011, 14 (5), pp.501-509

Bounds and approximation results for scheduling coupled-tasks with compatibility constraints

Authors: Rodolphe Giroudeau, Jean-Claude König, Benoit Darties, Gilles Simonin

Abstract: This article is devoted to propose some lower and upper bounds for the coupled-tasks scheduling problem in presence of compatibility constraints according to classical complexity hypothesis ($\mathcal{P} \neq \mathcal{NP}$, $\mathcal{ETH}$). Moreover, we develop an efficient polynomial-time approximation algorithm for the specific case for which the topology describing the compatibility constra… ▽ More This article is devoted to propose some lower and upper bounds for the coupled-tasks scheduling problem in presence of compatibility constraints according to classical complexity hypothesis ($\mathcal{P} \neq \mathcal{NP}$, $\mathcal{ETH}$). Moreover, we develop an efficient polynomial-time approximation algorithm for the specific case for which the topology describing the compatibility constraints is a quasi split-graph. △ Less

Submitted 7 June, 2017; originally announced June 2017.

Journal ref: 15th International Conference on Project Management and Scheduling, pp.94-97, 2016

Design and Analysis of Compressive Antenna Arrays for Direction of Arrival Estimation

Authors: Mohamed Ibrahim, Venkatesh Ramireddy, Anastasia Lavrenko, Jonas König, Florian Römer, Markus Landmann, Marcus Grossmann, Giovanni Del Galdo, Reiner S. Thomä

Abstract: In this paper we investigate the design of compressive antenna arrays for direction of arrival (DOA) estimation that aim to provide a larger aperture with a reduced hardware complexity by a linear combination of the antenna outputs to a lower number of receiver channels. We present a basic receiver architecture of such a compressive array and introduce a generic system model that includes differen… ▽ More In this paper we investigate the design of compressive antenna arrays for direction of arrival (DOA) estimation that aim to provide a larger aperture with a reduced hardware complexity by a linear combination of the antenna outputs to a lower number of receiver channels. We present a basic receiver architecture of such a compressive array and introduce a generic system model that includes different options for the hardware implementation. We then discuss the design of the analog combining network that performs the receiver channel reduction, and propose two design approaches. The first approach is based on the spatial correlation function which is a low-complexity scheme that in certain cases admits a closed-form solution. The second approach is based on minimizing the Cramer-Rao Bound (CRB) with the constraint to limit the probability of false detection of paths to a pre-specified level. Our numerical simulations demonstrate the superiority of the proposed optimized compressive arrays compared to the sparse arrays of the same complexity and to compressive arrays with randomly chosen combining kernels. △ Less

Submitted 11 November, 2016; originally announced November 2016.

Programming Language Features for Refinement

Authors: Jason Koenig, K. Rustan M. Leino

Abstract: Algorithmic and data refinement are well studied topics that provide a mathematically rigorous approach to gradually introducing details in the implementation of software. Program refinements are performed in the context of some programming language, but mainstream languages lack features for recording the sequence of refinement steps in the program text. To experiment with the combination of re… ▽ More Algorithmic and data refinement are well studied topics that provide a mathematically rigorous approach to gradually introducing details in the implementation of software. Program refinements are performed in the context of some programming language, but mainstream languages lack features for recording the sequence of refinement steps in the program text. To experiment with the combination of refinement, automated verification, and language design, refinement features have been added to the verification-aware programming language Dafny. This paper describes those features and reflects on some initial usage thereof. △ Less

Submitted 7 June, 2016; originally announced June 2016.

Comments: In Proceedings Refine'15, arXiv:1606.01344

ACM Class: D.2.4; D.3.2

Journal ref: EPTCS 209, 2016, pp. 87-106