Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking

• URL: http://arxiv.org/abs/2509.22215v1
• Date: Fri, 26 Sep 2025 11:29:53 GMT
• Title: Learn, Check, Test -- Security Testing Using Automata Learning and Model Checking
• Authors: Stefan Marksteiner, Mikael Sjödin, Marjan Sirjani,
• Abstract summary: We will investigate a cyber-physical systems as a black box using its external communication interface.<n>We first annotate the model with propositions by mapping context information from the respective protocol to the model.<n>We define generic security properties based on basic security requirements.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Cyber-physical systems are part of industrial systems and critical infrastructure. Therefore, they should be examined in a comprehensive manner to verify their correctness and security. At the same time, the complexity of such systems demands such examinations to be systematic and, if possible, automated for efficiency and accuracy. A method that can be useful in this context is model checking. However, this requires a model that faithfully represents the behavior of the examined system. Obtaining such a model is not trivial, as many of these systems can be examined only in black box settings due to, e.g., long supply chains or secrecy. We therefore utilize active black box learning techniques to infer behavioral models in the form of Mealy machines of such systems and translate them into a form that can be evaluated using a model checker. To this end, we will investigate a cyber-physical systems as a black box using its external communication interface. We first annotate the model with propositions by mapping context information from the respective protocol to the model using Context-based Proposition Maps (CPMs). We gain annotated Mealy machines that resemble Kripke structures. We then formally define a template, to transfer the structures model checker-compatible format. We further define generic security properties based on basic security requirements. Due to the used CPMs, we can instantiate these properties with a meaningful context to check a specific protocol, which makes the approach flexible and scalable. The gained model can be easily altered to introduce non-deterministic behavior (like timeouts) or faults and examined if the properties still. Lastly, we demonstrate the versatility of the approach by providing case studies of different communication protocols (NFC and UDS), checked with the same tool chain and the same security properties.

Related papers

• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• Interpretable Anomaly Detection in Encrypted Traffic Using SHAP with Machine Learning Models [0.0]
  This study aims to develop an interpretable machine learning-based framework for anomaly detection in encrypted network traffic.<n>Models are trained and evaluated on three benchmark encrypted traffic datasets.<n> SHAP visualizations successfully revealed the most influential traffic features contributing to anomaly predictions.
  arXiv  Detail & Related papers  (2025-05-22T05:50:39Z)
• Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes [1.6078581568133972]
  We propose a data-driven safety verification framework to verify system safety directly from noisy data.<n>Instead of trusting a single unreliable model, we construct a set of models that align with the observed data.<n>This model set is compactly represented using matrix zonotopes, enabling efficient computation and propagation of uncertainty.
  arXiv  Detail & Related papers  (2025-04-01T17:46:42Z)
• An Efficient Security Model for Industrial Internet of Things (IIoT) System Based on Machine Learning Principles [0.0]
  This paper presents a security paradigm for edge devices to defend against various internal and external threats.<n>The proposed security paradigm is found to be effective against various internal and external threats and can be applied to a low-cost single-board computer.
  arXiv  Detail & Related papers  (2025-02-10T14:20:13Z)
• Predicting the Performance of Black-box LLMs through Self-Queries [60.87193950962585]
  Large language models (LLMs) are increasingly relied on in AI systems, predicting when they make mistakes is crucial.<n>In this paper, we extract features of LLMs in a black-box manner by using follow-up prompts and taking the probabilities of different responses as representations.<n>We demonstrate that training a linear model on these low-dimensional representations produces reliable predictors of model performance at the instance level.
  arXiv  Detail & Related papers  (2025-01-02T22:26:54Z)
• Type-level Property Based Testing [0.0]
  We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. We are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics.
  arXiv  Detail & Related papers  (2024-07-17T16:43:41Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• Zero-shot Model Diagnosis [80.36063332820568]
  A common approach to evaluate deep learning models is to build a labeled test set with attributes of interest and assess how well it performs. This paper argues the case that Zero-shot Model Diagnosis (ZOOM) is possible without the need for a test set nor labeling.
  arXiv  Detail & Related papers  (2023-03-27T17:59:33Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Explaining RADAR features for detecting spoofing attacks in Connected Autonomous Vehicles [2.8153045998456188]
  Connected autonomous vehicles (CAVs) are anticipated to have built-in AI systems for defending against cyberattacks. Machine learning (ML) models form the basis of many such AI systems. We present a model that explains textitcertainty and textituncertainty in sensor input.
  arXiv  Detail & Related papers  (2022-03-01T00:11:46Z)
• SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
  We study the verification of parameterised multi-agent systems (MASs) In particular, we study whether unwanted states, characterised as a given state formula, are reachable in a given MAS.
  arXiv  Detail & Related papers  (2020-08-11T15:24:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.