PaperlayerView exact revision on arXiv

Source-linked AI summary

A Deterministic and Auditable AI Security Risk Assessment Framework with ATLAS Aligned Executable Rules and Formal Verification

Yixuan Huang, Basel Halak, Boojoong Kang

arXiv:2610.01436v1cs.AI

TL;DR

AI security assessments often lack reproducible mappings from observable engineering evidence to technique-level outcomes. This paper develops a deterministic, evidence-driven framework with formal guarantees and evaluates it on pinned open-source projects. Hardening shifts feasibility downward, although worst-case feasibility can persist when relevant controls remain absent from the evidence scope.

  • Problem

    Existing AI security assessments often rely on narrative or assessor-driven scoring and lack deterministic, auditable mappings from observable artefacts to stable risk outputs.

    Source: §1 · pp. 1–2

  • Method

    The framework normalises engineering artefacts into bounded Control ID scores, compiles ATLAS mitigation relations into technique-level predicates, and formally verifies evaluator properties.

    Source: §1 · p. 2, §7 · p. 24

  • Results

    Across five pinned projects, unified hardening consistently reduces aggregate feasibility summaries and shifts technique distributions downward, while worst-case contributions can persist when core controls remain missing.

    Source: §1 · p. 2, §7 · p. 24

  • Takeaways & Limitations

    Explicit rules connect observable evidence to technique outcomes for governance contexts where justification and replayability matter.

    Source: §7 · p. 24

    The repository-visible evidence scope omits many organisational controls, which are conservatively treated as missing and may overstate feasibility relative to a fully instrumented assessment.

    Source: §7 · p. 24

Abstract

from arXiv · show

Artificial intelligence systems are increasingly deployed in high impact and safety critical settings, yet security assessment remains difficult to reproduce and defend under audit. Existing approaches often rely on narrative checklists or assessor driven scoring, and they lack an explicit, machine evaluable mapping from observable engineering artefacts to stable technique level outcomes. We present an evidence driven AI security assessment framework that operationalises assessment as a deterministic decision function. The framework normalises heterogeneous artefacts into a project independent Control ID taxonomy scored on a bounded four level ordinal scale, compiles technique level predicates from a pinned MITRE ATLAS snapshot via an explicit mitigation to control mapping, and outputs technique indexed feasibility and impact levels with traceable links back to the triggering evidence. We package all normative choices as a versioned assessment policy object to support repeatable reassessment across snapshots. To ensure semantic correctness, we formally verify boundedness, totality, ordered semantic consistency, and monotonicity of the compiled evaluator over the full declared score domain. We evaluate the framework on five public open source AI projects pinned to explicit repository snapshots, quantify before and after changes under a unified hardening intervention, and validate responsiveness to real engineering changes through fork based implementations of Software Bill of Materials (SBOM) generation and Continuous integration (CI) security scanning gates. Results show consistent downward shifts in feasibility profiles under strengthened observable controls, while worst case residual feasibility persists when technique specific core controls remain absent from the evidence scope.

1 Introduction

AI security assessment lacks a reproducible mapping from observable engineering evidence to risk outputs. The paper proposes an evidence-driven framework that produces traceable technique-level results and evaluates how those results respond to strengthened controls.

1 Introduction

  • Existing assessments lack deterministic, auditable mappings from inspectable evidence to risk indicators, and often depend on subjective narratives or assessor-dependent semantics.These gaps hinder stable evidence normalisation and reproducibility under a fixed policy and system snapshot.Source: §1 · pp. 1–2
  • The framework normalises heterogeneous artefacts into project-independent Control IDs and compiles ATLAS mitigation relations into ordered predicates that return traceable technique-level feasibility and impact levels.The output links back to the engineering artefacts that triggered it.Source: §1 · p. 2
  • Formal verification establishes boundedness, totality, ordered semantic consistency, and monotonicity over the declared input domain.The assessment scope is non-probabilistic: it provides evidence-derived feasibility indicators and ordinal impact levels, not attack-frequency estimates or incident-rate predictions.Source: §1 · p. 2
  • Feasibility Impact Summary Index falls from 198 to 184 in KServe and from 324 to 266 in Cassava Example after unified hardening.The intervention sets the same subset of observed controls to rubric level 3 while leaving other observed controls unchanged.Source: §1 · p. 2
  • Techniques in feasibility band F = 0 increase from 2 to 9 in KServe and from 0 to 9 in vLLM after hardening.Worst-case technique risk remains unchanged when partial strengthening leaves relevant controls outside the intervention set unstrengthened.Source: §1 · p. 2

2 Background and Motivation

Prior governance frameworks, threat knowledge bases, and academic models organize AI risk concepts and sometimes quantify them, but the section identifies a shared operational gap: executable, auditable mappings from evidence to stable outcomes.

2 Background and Motivation

  • NIST AI RMF 1.0 and NCSC Machine Learning Security Principles offer lifecycle and governance guidance, but do not machine-evaluate artefacts into discrete, reproducible security outcomes.The CSA framework emphasizes documentation and scenario analysis, while Microsoft's assessment uses semi-quantitative matrices without formally specified executable rules.Source: §2 · p. 3
  • MITRE ATLAS structures adversarial techniques and mitigations, but does not specify artefact normalisation or executable decision logic.The practical gap is operationalising threat knowledge into a deterministic evaluator traceable to evidence.Source: §2 · p. 3
  • Academic methods add formal structure but retain limitations including subjective weights, domain-specific scope, Boolean feasibility, or focus on local robustness rather than system-level threats.Table 1 compares approaches across eight dimensions, including evidence grounding, control abstraction, executable semantics, traceability, and assessor dependence.Source: §2 · p. 4, Table 1 · p. 4
  • Across reviewed approaches, the section identifies no deterministic, formally specified mapping from observable control evidence to technique-indexed security outcomes.That operational gap motivates compiling governance intent into executable rules over Control IDs.Source: §2 · pp. 3–4

3 Methodology

The method turns inspectable engineering artefacts into technique-indexed feasibility and impact outputs, using Control IDs, compiled ATLAS-aligned rules, and a versioned policy for reproducible, traceable assessment.

3.1 Framework Overview and Problem Scope

  • A deterministic pipeline maps observable artefacts through Control IDs and ATLAS-aligned rules to technique-level feasibility and impact outputs with provenance links.The trace connects evaluated predicates to contributing controls and their source artefacts.Source: §3.1 · pp. 5–6, §3.4 · p. 9

3.2 Threat Model

  • The threat model covers supply-chain, API-level, and insider access positions; feasibility concerns operational realization under controls, not attempt frequency or strategic adaptation.The API attacker is limited to black-box interaction absent another compromise, while supply-chain and insider exposures are constrained by evidenced controls.Source: §3.2 · pp. 6–7

3.3 Raw Data Collection, Control ID Taxonomy, and Discrete Scoring

  • Inspectable engineering records are normalized into project-independent Control IDs, each tied to an artefact location and a repeatable four-level ordinal scoring rubric.The artefacts include software, pipeline, provenance, and deployment records; rubric design and application remain human specified.Source: §3.3 · p. 7

3.4 Rule Generation and Feasibility Computation

  • Pinned ATLAS technique–mitigation relations are compiled through explicit mandatory and compensating control mappings into ordered, traceable feasibility rules.Missing any core mitigation maximizes feasibility; optional mitigations provide defence in depth or governance reinforcement.Source: §3.4 · pp. 8–9

3.5 Impact Definition and Assignment

  • Impact is a stakeholder-anchored consequence level assigned independently of evidence-derived feasibility; experiments hold impact at level 2 across techniques and projects.This fixed assignment isolates feasibility changes, rather than providing context-calibrated consequence analysis.Source: §3.5 · p. 10

3.6 Assessment Policy Configuration for Reproducibility and Auditability

  • A versioned policy object records the ATLAS snapshot, evidence bindings, rubrics, mappings, technique profiles, and impact configuration for reassessment.Policy updates trigger recompilation and formal re-verification, while reports record the policy identifier and configuration hash.Source: §3.6 · pp. 10–11

4 Formal Verification

The evaluator is checked over its bounded ordinal input domain by searching for counterexamples to four semantic properties. All 302 generated proof obligations were discharged without a counterexample.

4.1 Property selection

  • The four required properties are boundedness, totality, ordered semantic consistency, and monotonicity under strengthened controls.Together they keep outputs in range, define an outcome for every admissible input, respect rule priority, and prevent stronger controls from increasing feasibility.Source: §4.1 · pp. 11–12, §4.3 · p. 13

4.2 Verification procedure

  • The verification procedure encodes each property’s negation as a satisfiability query over scores in {0, 1, 2, 3}.A satisfiable query supplies a replayable counterexample; an unsatisfiable query discharges the property over the declared domain.Source: §4.2 · p. 12
  • Boundedness requires mitigation strengths and feasibility outputs to remain within the four-level scale, preserving valid inputs to downstream aggregation.The solver searches for an assignment that puts either intermediate or final values outside {0, 1, 2, 3}.Source: §4.2 · p. 12
  • Totality rules out inputs with no matching predicate, while ordered consistency requires the selected level to be witnessed and all higher-priority predicates to be false.These checks exclude silent no-decision cases and miswitnessed or priority-inverted outputs.Source: §4.2 · p. 12

4.3 Verification results

  • The 302 obligations comprise |M| + 5|T| queries across mitigation boundedness and technique-level boundedness, totality, ordered consistency, and monotonicity.Ordered consistency contributes two obligations per technique; each of the other technique-level properties contributes one.Source: §4.3 · p. 13
  • The resulting assurance applies to the current compiled rule base and its declared bounded input domain.The authors characterize these checks as a minimal set of semantic correctness requirements for reproducible and auditable deployment.Source: §4.3 · p. 13
  • 302 proof obligations yielded no counterexamples, discharging all obligations with a 100% pass rate.The obligations are generated for compiled mitigation evaluators and technique-level decision semantics, not individual score assignments.Source: §4.3 · p. 13, Table 3 · p. 14

5 Experiment

The experiment assesses counterfactual hardening and implemented fork changes on pinned snapshots, then uses feasibility- and impact-based metrics to characterize assessment changes.

5.1 Setup

  • Five public projects and a MITRE ATLAS snapshot are pinned; the evaluation includes 54 assessable techniques across 15 of 62 controls observable in repository snapshots.Techniques without mapped controls in scope are excluded, and absent artefacts for included controls score zero, a convention that conservatively increases feasibility.Source: §5.1 · p. 14, Table 4 · p. 15
  • The controlled intervention raises a shared subset of controls to level 3 while leaving other scores unchanged; impacts remain fixed for before-and-after comparisons.Tables 5 and 6 report baseline control scores and counterfactual changes under unified hardening.Source: §5.1 · p. 15
  • Fork-based tests add committed SBOM generation and a CodeQL CI security-analysis gate, then rescore only from newly observable artefacts.The full assessment pipeline is rerun on pinned fork commits without manual score edits.Source: §5.1 · p. 15
  • A second assessor independently rescored selected controls for two projects; disagreements were adjudicated against the same evidence, retaining the lower score when ambiguity remained.The study reports per-control comparisons and agreement statistics.Source: §5.1 · p. 15, Table 8 · p. 17

5.2 Metrics

  • Because feasibility and impact are four-level ordinal scores, scalar aggregates are heuristic summaries rather than calibrated real-world risk measures.Source: §5.2 · p. 16
  • The analysis also reports maximum technique contribution and the share of techniques in the high-feasibility, high-impact region, using thresholds of 2.That region covers levels 2 and 3 on the four-level ordinal scale.Source: §5.2 · pp. 17–18
  • The metrics include a high-risk share that reduces to the fraction of techniques with feasibility at least 2, alongside FISI and absolute and relative reductions.Impact is fixed at level 2 for all techniques and projects in this setup.Source: §5.2 · pp. 16, 18
  • Normalized technique-contribution profiles are summarized by entropy for concentration and Jensen–Shannon divergence for before-and-after profile change.Lower entropy means contributions are concentrated in fewer techniques; higher entropy indicates a more diffuse profile.Source: §5.2 · p. 18

6 Results

Unified hardening reduced aggregate feasibility across projects but left worst-case feasibility unchanged; assessor agreement, policy sensitivity, and concrete fork experiments qualify how to interpret those shifts.

6.1 Overall Hardening Effect Across Projects

  • Across five projects, unified hardening reduced FISI for all and HRS for four, but WCR stayed at 6, leaving at least one technique at feasibility 3.HRS examples include Ultralytics (0.9815 to 0.8333), TorchServe (0.9259 to 0.8333), Cassava Example (1.0000 to 0.8333), and unchanged KServe (0.5185).Source: §6.1 · pp. 18–19, Table 9 · p. 19

6.2 Interrater consistency

  • Exact assessor agreement was 60.0%, while 96.7% of scores agreed within one level; disagreements often involved documentation without inspectable enforcement artefacts.Weighted Cohen’s κ was 0.58 with linear weights and 0.73 with quadratic weights; adjudicated ambiguous cases received the lower score.Source: §6.2 · p. 19, Table 10 · p. 20

6.3 Sensitivity to Alternative Policy Mappings

  • Hardening reduced FISI for all five projects under Base and Permissive mappings, but Strict mapping saturated feasibility and produced no change.Relative FISI reductions spanned 0.0707–0.1790 under Base and 0.1042–0.2346 under Permissive; Strict yielded FISI of 324 before and after.Source: §6.3 · p. 20, Table 11 · p. 21

6.4 Fork based Concrete Control Implementation

  • Forks implementing SBOM generation and a CodeQL CI gate produced small, auditable feasibility shifts without manual score edits.In both KServe and vLLM, one technique moved from F=1 to F=0; remaining maximum-feasibility cases were tied to other missing core controls.Source: §6.4 · pp. 21–22, Table 14 · p. 23

6.5 Feasibility Shifts

  • Unified hardening increased the count at F=0 across projects, while migration patterns differed and thresholded HRS could miss within-band improvements.KServe’s F=3 and F=2 bands were unchanged; Cassava Example’s F=3 count fell from 54 to 43.Source: Table 15 · p. 23, §6.5 · p. 23

7 Conclusion

The paper concludes that its evidence-driven, ATLAS-aligned assessment framework produces traceable technique-level outcomes and formally verified evaluation semantics. Tests show feasibility reductions under strengthened observable controls, while repository-visible evidence and policy choices bound what the results represent.

7 Conclusion

  • The framework maps inspectable artefacts into project-independent Control IDs and evaluates ATLAS-aligned technique rules with explicit, traceable semantics.The outputs are repeatable across runs and comparable across projects under the same policy configuration.Source: §7 · pp. 23–24
  • Formal verification establishes boundedness, totality, ordered semantic consistency, and monotonicity across the declared input domain.Monotonicity means strengthening controls cannot increase assessed feasibility under the same semantics.Source: §7 · p. 24
  • Across five pinned open-source projects, strengthened observable controls reduced feasibility, but worst-case residuals persisted when technique-specific core controls were missing.Forked implementations adding SBOM generation and CI security gates produced shifts tied to newly observable evidence.Source: §7 · p. 24
  • Repository-visible evidence leaves organisational controls outside the assessment scope, which are treated as missing and may overstate feasibility.Examples include internal reviews, supplier due diligence, runbooks, incident exercises, and monitoring procedures.Source: §7 · p. 24
  • Results also depend on policy configuration choices, while scalar aggregation of ordinal feasibility and impact levels is only a heuristic summary.The paper therefore emphasizes ordinal-preserving metrics and reports FISI as a secondary aid under a fixed policy.Source: §7 · p. 24
  • Future work will broaden evidence adapters beyond repository snapshots and evaluate more projects and deployment settings.The authors also plan policy calibration procedures that preserve discriminative power while remaining conservative for the intended governance context.Source: §7 · pp. 24–25

A Control Scoring Rubric

Table 16 is identified as the Control ID scoring rubric; the supplied caption specifies a scale from 0 (weakest) to 3 (strongest).

A Control Scoring Rubric

  • Table 16 presents the Control ID scoring rubric on a scale where 0 is weakest and 3 is strongest.Source: Table 16 · p. 25
Loading 2610.01436v1…