arXiv subjects

Andreas Lindner

Publications and source records attributed to Andreas Lindner.

12 recordsLinked to original sources

arXiv2026

NESSA: a compact 14 MeV D-T neutron source facility at Uppsala University

The NESSA (Neutron Source in Uppsala) facility hosts a compact 14 MeV deuterium-tritium sealed tube neutron generator at the {\AA}ngstr\"om Laboratory, Uppsala University. The generator, housed in a bunker inside the FREIA hall, reaches a maximum yield of $4.7\times10^{8}$ n/s. This paper describes the facility: the generator, the bunker and its shielding, the detector systems, and the Monte Carlo models used to characterize the neutron field. We also report the first commissioning measurements: yield calibration with $^{93}$Nb activation foils, fission chamber response at two positions, and simulated air and structural activation. Initial indium foil activations and single event effect (SEE) tests on silicon devices are also presented. The facility will be used for nuclear data measurements, neutron detector response studies, moderation and thermalization experiments, irradiation testing of electronics as well as for training and education.

physics.ins-det↗

arXiv2025

Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA

Many types of formal verification establish properties about abstract high-level program representations, leaving a large gap to programs at runtime. Although gaps can sometimes be narrowed by techniques such as refinement, a verified program's trusted computing base may still include compilers and inlined assembly. In contrast, verification of binaries following an Instruction Set Architecture (ISA) such as RISC-V can ensure that machine code behaves as expected on real hardware. While binary analysis is useful and sometimes even necessary for ensuring trustworthiness of software systems, existing tools do not have a formal foundation or lack automation for verification. We present a workflow and toolchain based on the HOL4 theorem prover and the HolBA binary analysis library for trustworthy formal verification of RISC-V binaries. The toolchain automates proofs of binary contracts by forward symbolic execution of programs in HolBA's intermediate language, BIR. We validated our toolchain by verifying correctness of RISC-V binaries with (1) an implementation of the ChaCha20 stream cipher and (2) hand-written assembly for context switching in an operating system kernel.

cs.LO↗

arXiv2023

Beyond Over-Protection: A Targeted Approach to Spectre Mitigation and Performance Optimization

Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using slh that often results in over-protection, which incurs performance overhead. We extended an existing side-channel model validation framework, Scam-V, to check the vulnerability of programs to Spectre-PHT attacks and optimize the protection of programs using the slh approach. We illustrate the efficacy of Scam-V by first demonstrating that it can automatically identify Spectre vulnerabilities in real programs, e.g., fragments of crypto-libraries. We then develop an optimization mechanism that validates the necessity of slh hardening w.r.t. the target platform. Our experiments showed that hardening introduced by LLVM in most cases could be significantly improved when the underlying microarchitecture properties are considered.

cs.CR↗

arXiv2023

Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification

Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when certifying properties of binary (machine) code in trustworthy systems, e.g., cryptographic routines. We present a theory of forward symbolic execution for unstructured programs suitable for use in theorem provers that enables automated verification of both functional and non-functional program properties. The theory's foundation is a set of inference rules where each member corresponds to an operation in a symbolic execution engine. The rules are designed to give control over the tradeoff between the preservation of precision and introduction of overapproximation. We instantiate our theory for BIR, a previously proposed intermediate language for binary analysis. We demonstrate how symbolic executors can be constructed for BIR with common optimizations such as pruning of infeasible symbolic states. We implemented our theory in the HOL4 theorem prover using the HolBA binary analysis library, obtaining machine-checked proofs of soundness of symbolic execution for BIR. We practically evaluated two applications of our theory: verification of functional properties of RISC-V binaries and verification of execution time bounds of programs running on the ARM Cortex-M0 processor. The evaluation shows that such verification can be automated with moderate overhead on medium-sized programs.

cs.PL↗

arXiv2022

HEWES: Heisenberg-Euler Weak-Field Expansion Simulator

Vacuum polarization, a key prediction of quantum theory, can cause a variety of intriguing phenomena that can be triggered by high-intensity laser pulses. The Heisenberg-Euler theory of the quantum vacuum supplements Maxwell's theory of electromagnetism with nonlinear photon-photon interactions mediated by vacuum fluctuations. This work presents a numerical solver for the leading weak-field Heisenberg-Euler corrections. The present code implementation reaches an accuracy of order thirteen in the numerical scheme and takes into account up to six-photon interactions. Since theoretical approaches are limited to approximations and the experimental requirements for signal detection are high, the need for support from the numerical side is apparent.

hep-ph↗

arXiv2022

Matching to Higgs-Compositeness and Renormalization of the Higgs-Electroweak Chiral Lagrangian extended by a Scalar Singlet

We match the electroweak chiral Lagrangian with two singlet scalars to the next-to-minimal composite Higgs model with $ SO(6)/SO(5) $ coset structure and extract the scalar divergences to one loop. Assuming the additional scalar to be heavy, we integrate it out and perform a matching to the well-established electroweak chiral Lagrangian with one light Higgs.

hep-ph↗

arXiv2022

One-Loop Renormalization of the Higgs Sector of the Electroweak Chiral Lagrangian extended by N Scalar Singlets

The framework of the electroweak chiral Lagrangian with a light Higgs is extended by an additional scalar and then generalized to N scalars in the Higgs sector. Divergences from scalar fluctuations are renormalized up to one loop using the background field method. The results are crosschecked against the case of one scalar. A subset of the divergences is demonstrated and crosschecked diagrammatically. Together with the complete one-loop renormalization of the electroweak chiral theory with one light Higgs conducted previously, this constitutes a renormalization framework of any pure scalar extension to the electroweak chiral theory.

hep-ph↗

arXiv2021

Numerical Simulations of the Nonlinear Quantum Vacuum in the Heisenberg-Euler Weak-Field Expansion

The Heisenberg-Euler theory of the quantum vacuum supplements Maxwell's theory of electromagnetism with nonlinear light-light interactions. These originate in vacuum fluctuations, a key prediction of quantum theory, and can be triggered by high-intensity laser pulses, causing a variety of intriguing phenomena. A highly accurate numerical scheme for solving the nonlinear equations due to the leading orders of the Heisenberg-Euler weak-field expansion is presented. The algorithm possesses an almost linear vacuum dispersion relation even for comparably small wavelengths and incorporates a nonphysical modes filter. The implemented solver is tested in one spatial dimension against a set of known analytical results for vacuum birefringence and harmonic generation. More complex scenarios for harmonic generation are demonstrated in two and three spatial dimensions.

physics.comp-ph↗

arXiv2020

Speculative Leakage in ARM Cortex-A53

The recent Spectre attacks have demonstrated that modern microarchitectural optimizations can make software insecure. These attacks use features like pipelining, out-of-order and speculation to extract information about the memory contents of a process via side-channels. In this paper we demonstrate that Cortex-A53 is affected by speculative leakage even if the microarchitecture does not support out-of-order execution. We named this new class of vulnerabilities SiSCloak.

cs.CR↗

arXiv2020

Validation of Abstract Side-Channel Models for Computer Architectures

Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior.

cs.CR↗

arXiv2019

TrABin: Trustworthy Analyses of Binaries

Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, and a set of architecture independent analyses that process the intermediate representation. The usage of these platforms to verify software introduces the need for trusting both the correctness of the translation from binary code to intermediate language (called transpilation) and the correctness of the analyses. Achieving a high degree of trust is challenging since the transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encodings (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). Similarly, analyses can use complex transformations (e.g. loop unrolling) and simplifications (e.g. partial evaluation) of the artifacts, whose bugs can jeopardize correctness of the results. We overcome these problems by developing a binary analysis platform on top of the interactive theorem prover HOL4. First, we formally model a binary intermediate language and we prove correctness of several supporting tools (i.e. a type checker). Then, we implement two proof-producing transpilers, which respectively translate ARMv8 and CortexM0 programs to the intermediate language and generate a certificate. This certificate is a HOL4 proof demonstrating correctness of the translation. As demonstrating analysis, we implement a proof-producing weakest precondition generator, which can be used to verify that a given loop-free program fragment satisfies a contract. Finally, we use an AES encryption implementation to benchmark our platform.

cs.PL↗

arXiv2018

Sound Transpilation from Binary to Machine-Independent Code

In order to handle the complexity and heterogeneity of mod- ern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent intermediate representa- tions. The usage of these platforms to verify systems down to binary-level is appealing due to the high degree of automation they provide. How- ever, it introduces the need for trusting the correctness of the translation from binary code to intermediate language. Achieving a high degree of trust is challenging since this transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encoding (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). We overcome these problems by formally modeling one of such intermediate languages in the interactive theorem prover HOL4 and by implementing a proof- producing transpiler. This tool translates ARMv8 programs to the in- termediate language and generates a HOL4 proof that demonstrates the correctness of the translation in the form of a simulation theorem. We also show how the transpiler theorems can be used to transfer properties verified on the intermediate language to the binary code.

cs.PL↗