arXiv subjects

Gudmund Grov

Publications and source records attributed to Gudmund Grov.

17 recordsLinked to original sources

arXiv2026

CCR: Towards a Common, Quality-Gated CACAO Integrations Registry for European Cybersecurity Automation

Standardised, machine-readable cybersecurity playbooks provide a basis for portable, shareable, and reusable incident-response logic. OASIS CACAO provides a vendor-neutral representation for such playbooks, but not the product-specific integration artefacts needed to invoke external products and services. We introduce the Common CACAO Registry (CCR), an open, provenance-aware registry of CACAO HTTP-API connector envelopes. Each envelope captures an API operation's command, inputs, target, authentication-related information, provenance, validation evidence, and maturity metadata. CCR is quality-gated, with acceptance requiring both CACAO v2 schema validity and a mean back-validation score of at least 0.8 against the source OpenAPI operation, while a six-level maturity model records progressively stronger evidence and distinguishes gate acceptance from operational readiness. To seed CCR, we develop a hybrid OpenAPI-to-CACAO pipeline. Deterministic code extracts source-derived interface facts, generates identifiers, wires cross-references, and validates structure, while a constrained LLM provides bounded semantic enrichment, including action naming, authentication interpretation, and CACAO activity annotation. Evaluation across eight security APIs yields 713 CACAO-schema-valid envelopes with a mean back-validation score of 91.5%, of which 675 produce well-formed, dispatchable HTTP requests in a local harness. Comparison with a deterministic rule-based baseline shows that mechanical API structure is preserved more reliably through rule-based translation, while the LLM contributes bounded semantic enrichment, most notably CACAO activity annotation. Together, these results support CCR as reusable integration infrastructure for CACAO action steps and as an initial foundation for a broader common European registry.

cs.CR↗

arXiv2026

CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness

LLM-based agents generate and execute multi-step plans that invoke external tools which can access private data or execute commands. In this setting, security is a property of the entire execution that a plan creates, not just any single step. The plan itself is a critical artefact that captures the tool calls, control flow, and data dependencies. We present CaMeLoT, a complement to CaMeL, an existing defence against prompt injection in tool-using LLM agents. CaMeLoT extends CaMeL by adding a static verification layer that checks an agent's plan before any tool is invoked. CaMeLoT translates a generated plan into a finite-state transition system, labels it with tool calls, provenance and taint information, and checks it against temporal policies expressed in CTL using the nuXmv model checker. Because verification happens before execution, unsafe plans are rejected without using LLM calls or tool calls, saving tokens that runtime could have cost, as well as the need to unwind changes or teardown temporary sandboxes. When a verification fails, the model checker returns a counterexample to give feedback to the agent to repair the plan. We evaluate CaMeLoT on policies derived from the AgentDojo benchmark, SOC workflows, and prompt-extraction experiments, showing that it verifies a broad class of temporal properties before execution while preserving CaMeL's runtime-checkable coverage.

cs.CR↗

arXiv2026

Towards Agentic Investigation of Security Alerts

Security analysts are overwhelmed by the volume of alerts and the low context provided by many detection systems. Early-stage investigations typically require manual correlation across multiple log sources, a task that is usually time-consuming. In this paper, we present an experimental, agentic workflow that leverages large language models (LLMs) augmented with predefined queries and constrained tool access (structured SQL over Suricata logs and grep-based text search) to automate the first stages of alert investigation. The proposed workflow integrates queries to provide an overview of the available data, and LLM components that selects which queries to use based on the overview results, extracts raw evidence from the query results, and delivers a final verdict of the alert. Our results demonstrate that the LLM-powered workflow can investigate log sources, plan an investigation, and produce a final verdict that has a significantly higher accuracy than a verdict produced by the same LLM without the proposed workflow. By recognizing the inherent limitations of directly applying LLMs to high-volume and unstructured data, we propose combining existing investigation practices of real-world analysts with a structured approach to leverage LLMs as virtual security analysts, thereby assisting and reducing the manual workload.

cs.CR↗

arXiv2026

Detecting and Eliminating Neural Network Backdoors Through Active Paths with Application to Intrusion Detection

Machine learning backdoors have the property that the machine learning model should work as expected on normal inputs, but when the input contains a specific $\textit{trigger}$, it behaves as the attacker desires. Detecting such triggers has been proven to be extremely difficult. In this paper, we present a novel and explainable approach to detect and eliminate such backdoor triggers based on active paths found in neural networks. We present promising experimental evidence of our approach, which involves injecting backdoors into a machine learning model used for intrusion detection.

cs.CR↗

arXiv2025

A Graph-Based Approach to Alert Contextualisation in Security Operations Centres

Interpreting the massive volume of security alerts is a significant challenge in Security Operations Centres (SOCs). Effective contextualisation is important, enabling quick distinction between genuine threats and benign activity to prioritise what needs further analysis. This paper proposes a graph-based approach to enhance alert contextualisation in a SOC by aggregating alerts into graph-based alert groups, where nodes represent alerts and edges denote relationships within defined time-windows. By grouping related alerts, we enable analysis at a higher abstraction level, capturing attack steps more effectively than individual alerts. Furthermore, to show that our format is well suited for downstream machine learning methods, we employ Graph Matching Networks (GMNs) to correlate incoming alert groups with historical incidents, providing analysts with additional insights.

cs.CR↗

arXiv2025

LLM-Powered Intent-Based Categorization of Phishing Emails

Phishing attacks remain a significant threat to modern cybersecurity, as they successfully deceive both humans and the defense mechanisms intended to protect them. Traditional detection systems primarily focus on email metadata that users cannot see in their inboxes. Additionally, these systems struggle with phishing emails, which experienced users can often identify empirically by the text alone. This paper investigates the practical potential of Large Language Models (LLMs) to detect these emails by focusing on their intent. In addition to the binary classification of phishing emails, the paper introduces an intent-type taxonomy, which is operationalized by the LLMs to classify emails into distinct categories and, therefore, generate actionable threat information. To facilitate our work, we have curated publicly available datasets into a custom dataset containing a mix of legitimate and phishing emails. Our results demonstrate that existing LLMs are capable of detecting and categorizing phishing emails, underscoring their potential in this domain.

cs.CR↗

arXiv2024

Exploring reinforcement learning for incident response in autonomous military vehicles

Unmanned vehicles able to conduct advanced operations without human intervention are being developed at a fast pace for many purposes. Not surprisingly, they are also expected to significantly change how military operations can be conducted. To leverage the potential of this new technology in a physically and logically contested environment, security risks are to be assessed and managed accordingly. Research on this topic points to autonomous cyber defence as one of the capabilities that may be needed to accelerate the adoption of these vehicles for military purposes. Here, we pursue this line of investigation by exploring reinforcement learning to train an agent that can autonomously respond to cyber attacks on unmanned vehicles in the context of a military operation. We first developed a simple simulation environment to quickly prototype and test some proof-of-concept agents for an initial evaluation. This agent was then applied to a more realistic simulation environment and finally deployed on an actual unmanned ground vehicle for even more realism. A key contribution of our work is demonstrating that reinforcement learning is a viable approach to train an agent that can be used for autonomous cyber defence on a real unmanned ground vehicle, even when trained in a simple simulation environment.

cs.CR↗

arXiv2024

On the use of neurosymbolic AI for defending against cyber attacks

It is generally accepted that all cyber attacks cannot be prevented, creating a need for the ability to detect and respond to cyber attacks. Both connectionist and symbolic AI are currently being used to support such detection and response. In this paper, we make the case for combining them using neurosymbolic AI. We identify a set of challenges when using AI today and propose a set of neurosymbolic use cases we believe are both interesting research directions for the neurosymbolic AI community and can have an impact on the cyber security field. We demonstrate feasibility through two proof-of-concept experiments.

cs.AI↗

arXiv2017

DAReing to reduce the annotation overheads of verified programs

Modern program verifiers use the same uniform program text to both specify and implement programs. The program text is also used to provide the necessary guidance to ensure that the program satisfies its specification. The amount of guidance required is often called the annotation overhead. This can be high and is often seen as a hindrance for wider use of program verifiers, as development time is increased and the guidance may obfuscate the program text. In this paper we introduce the DARe tool, which automatically removes as much unnecessary guidance as possible for the Dafny program verifier. The tool is integrated with the Dafny IDE. To evaluate DARe, we apply it to 252 programs from the Dafny library and analyse the degree to which it is able to remove unnecessary guidance. Our results are very encouraging as a staggering 88% of the guidance can be removed.

cs.SE↗

arXiv2016

Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC

The use of a functional language to implement proof strategies as proof tactics in interactive theorem provers, often provides short, concise and elegant implementations. Whilst being elegant, the use of higher order features and combinator languages often results in a very procedural view of a strategy, which may deviate significantly from the high-level ideas behind it. This can make a tactic hard to understand and hence difficult to to debug and maintain for experts and non-experts alike: one often has to tear apart complex combinations of lower level tactics manually in order to analyse a failure in the overall strategy. In an industrial technology transfer project, we have been working on porting a very large and complex proof tactic into PSGraph, a graphical language for representing proof strategies, supported by the Tinker tool. The goal of this work is to improve understandability and maintainability of tactics. Motivated by some initial successes with this, we here extend PSGraph with additional features for development and debugging. Through the re-implementation and refactoring of several existing tactics, we demonstrates the advantages of PSGraph compared with a typical linear (term-based) tactic language with respect to debugging, readability and maintenance. In order to act as guidance for others, we give a fairly detailed comparison of the user experience with the two approaches. The paper is supported by a web page providing further details about the implementation as well as interactive illustrations of the examples.

cs.LO↗

arXiv2016

Semi-Automated Design Space Exploration for Formal Modelling

Refinement based formal methods allow the modelling of systems through incremental steps via abstraction. Discovering the right levels of abstraction, formulating correct and meaningful invariants, and analysing faulty models are some of the challenges faced when using this technique. Here, we propose Design Space Exploration, an approach that aims to assist a designer by automatically providing high-level modelling guidance in real-time. More specifically, through the combination of common patterns of modelling with techniques from automated theory formation and automated reasoning, different design alternatives are explored and suitable models that deal with faults are proposed.

cs.SE↗

arXiv2015

Automating change of representation for proofs in discrete mathematics

Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is, therefore, a need for the development of better tools to mechanise and automate formal and logically sound changes of representation. In this paper we look at examples of representational transformations in discrete mathematics, and show how we have used Isabelle's Transfer tool to automate the use of these transformations in proofs. We give a brief overview of a general theory of transformations that we consider appropriate for thinking about the matter, and we explain how it relates to the Transfer package. We show our progress towards developing a general tactic that incorporates the automatic search for representation within the proving process.

cs.AI↗

arXiv2014

Tinker, tailor, solver, proof

We introduce Tinker, a tool for designing and evaluating proof strategies based on proof-strategy graphs, a formalism previously introduced by the authors. We represent proof strategies as open-graphs, which are directed graphs with additional input/output edges. Tactics appear as nodes in a graph, and can be `piped' together by adding edges between them. Goals are added to the input edges of such a graph, and flow through the graph as the strategy is evaluated. Properties of the edges ensure that only the right `type' of goals are accepted. In this paper, we detail the Tinker tool and show how it can be integrated with two different theorem provers: Isabelle and ProofPower.

cs.LO↗

arXiv2014

Some Ideas for Program Verifier Tactics

A program verifier is a tool that can be used to verify that a "contract" for a program holds - i.e. given a precondition the program guarantees that a given postcondition holds - by only working at the level of the annotated program. An alternative approach is to use an interactive theorem prover, which enables users to encode common proof patterns as special programs called "tactics". This offers more flexibility than program verifiers, but at the expense of skills required by the user. Here, we add such flexibility to program verifiers by developing "tactics" as a form of program refactoring called DTacs. A formal characterisation and set of examples are given, illustrated with a case study from NASA.

cs.SE↗

arXiv2013

A Graphical Language for Proof Strategies

Complex automated proof strategies are often difficult to extract, visualise, modify, and debug. Traditional tactic languages, often based on stack-based goal propagation, make it easy to write proofs that obscure the flow of goals between tactics and are fragile to minor changes in input, proof structure or changes to tactics themselves. Here, we address this by introducing a graphical language called PSGraph for writing proof strategies. Strategies are constructed visually by "wiring together" collections of tactics and evaluated by propagating goal nodes through the diagram via graph rewriting. Tactic nodes can have many output wires, and use a filtering procedure based on goal-types (predicates describing the features of a goal) to decide where best to send newly-generated sub-goals. In addition to making the flow of goal information explicit, the graphical language can fulfil the role of many tacticals using visual idioms like branching, merging, and feedback loops. We argue that this language enables development of more robust proof strategies and provide several examples, along with a prototype implementation in Isabelle.

cs.LO↗

arXiv2013

Machine Learning in Proof General: Interfacing Interfaces

We present ML4PG - a machine learning extension for Proof General. It allows users to gather proof statistics related to shapes of goals, sequences of applied tactics, and proof tree structures from the libraries of interactive higher-order proofs written in Coq and SSReflect. The gathered data is clustered using the state-of-the-art machine learning algorithms available in MATLAB and Weka. ML4PG provides automated interfacing between Proof General and MATLAB/Weka. The results of clustering are used by ML4PG to provide proof hints in the process of interactive proof development.

cs.AI↗

arXiv2013

Towards Automated Proof Strategy Generalisation

The ability to automatically generalise (interactive) proofs and use such generalisations to discharge related conjectures is a very hard problem which remains unsolved. Here, we develop a notion of goal types to capture key properties of goals, which enables abstractions over the specific order and number of sub-goals arising when composing tactics. We show that the goal types form a lattice, and utilise this property in the techniques we develop to automatically generalise proof strategies in order to reuse it for proofs of related conjectures. We illustrate our approach with an example.

cs.LO↗