Neural networks are a powerful class of non-linear functions. However, their black-box nature makes it difficult to explain their behaviour and certify their safety. Abstraction techniques address ...this challenge by transforming the neural network into a simpler, over-approximated function. Unfortunately, existing abstraction techniques are slack, which limits their applicability to small local regions of the input domain. In this paper, we propose Global Interval Neural Network Abstractions with Center-Exact Reconstruction (GINNACER). Our novel abstraction technique produces sound over-approximation bounds over the whole input domain while guaranteeing exact reconstructions for any given local input. Our experiments show that GINNACER is several orders of magnitude tighter than state-of-the-art global abstraction techniques, while being competitive with local ones.
Abstract
This work describes an approach for synthesizing state-feedback controllers for discrete-time systems, taking into account performance aspects. The proposed methodology is based on ...counterexample-guided inductive synthesis (CEGIS), producing safe controllers based on step response performance requirements, such as settling time and maximum-overshoot. Controller candidates are generated through constrained optimization based on genetic algorithms. Each iteration that does not satisfy the initial system requirements is learned as a failed result and then used in another attempt. During the verification phase, it is considered the controller fragility to ensure deployable implementations. Such an approach assists the discrete-time control system design since weaknesses occur during implementation on digital platforms, where systems that meet design requirements are employed. The proposed method is implemented in DSVerifier, a tool that uses bounded (and unbounded) model checking based on satisfiability modulo theories. Experimental results showed that our approach is practical and sound regarding the synthesis of discrete state-feedback control systems that present performance requirements. It considers finite word-length effects, unlike other methods that routinely ignore them.
The field of Natural Language Processing (NLP) is currently undergoing a revolutionary transformation driven by the power of pre-trained Large Language Models (LLMs) based on groundbreaking ...Transformer architectures. As the frequency and diversity of cybersecurity attacks continue to rise, the importance of incident detection has significantly increased. IoT devices are expanding rapidly, resulting in a growing need for efficient techniques to autonomously identify network-based attacks in IoT networks with both high precision and minimal computational requirements. This paper presents SecurityBERT, a novel architecture that leverages the Bidirectional Encoder Representations from Transformers (BERT) model for cyber threat detection in IoT networks. During the training of SecurityBERT, we incorporated a novel privacy-preserving encoding technique called Privacy-Preserving Fixed-Length Encoding (PPFLE). We effectively represented network traffic data in a structured format by combining PPFLE with the Byte-level Byte-Pair Encoder (BBPE) Tokenizer. Our research demonstrates that SecurityBERT outperforms traditional Machine Learning (ML) and Deep Learning (DL) methods, such as Convolutional Neural Networks (CNNs) or Recurrent Neural Networks (RNNs), in cyber threat detection. Employing the Edge-IIoTset cybersecurity dataset, our experimental analysis shows that SecurityBERT achieved an impressive 98.2% overall accuracy in identifying fourteen distinct attack types, surpassing previous records set by hybrid solutions such as GAN-Transformer-based architectures and CNN-LSTM models. With an inference time of less than 0.15 seconds on an average CPU and a compact model size of just 16.7MB, SecurityBERT is ideally suited for real-life traffic analysis and a suitable choice for deployment on resource-constrained IoT devices.
Model checking C++ programs Monteiro, Felipe R.; Gadelha, Mikhail R.; Cordeiro, Lucas C.
Software testing, verification & reliability,
January 2022, 2022-01-00, 20220101, Letnik:
32, Številka:
1
Journal Article
Recenzirano
Odprti dostop
Summary
In the last three decades, memory safety issues in system programming languages such as C or C++ have been one of the most significant sources of security vulnerabilities. However, there ...exist only a few attempts with limited success to cope with the complexity of C++ program verification. We describe and evaluate a novel verification approach based on bounded model checking (BMC) and satisfiability modulo theories (SMT) to verify C++ programs. Our verification approach analyses bounded C++ programs by encoding into SMT various sophisticated features that the C++ programming language offers, such as templates, inheritance, polymorphism, exception handling, and the Standard Template Libraries. We formalize these features within our formal verification framework using a decidable fragment of first‐order logic and then show how state‐of‐the‐art SMT solvers can efficiently handle that. We implemented our verification approach on top of ESBMC. We compare ESBMC to LLBMC and DIVINE, which are state‐of‐the‐art verifiers to check C++ programs directly from the LLVM bitcode. Experimental results show that ESBMC can handle a wide range of C++ programs, presenting a higher number of correct verification results. Additionally, ESBMC has been applied to a commercial C++ application in the telecommunication domain and successfully detected arithmetic‐overflow errors, which could potentially lead to security vulnerabilities.
ESBMC is a permissively licensed open‐source context‐bounded model checker for the verification of single‐ and multi‐threaded C and C++ programs. It can verify both predefined safety properties (e.g., bounds check, pointer safety, and arithmetic overflow) and user‐defined program assertions.
Counterexample Guided Neural Network Quantization Refinement Matos, Joao Batista P.; de Lima Filho, Eddie B.; Bessa, Iury ...
IEEE transactions on computer-aided design of integrated circuits and systems,
04/2024, Letnik:
43, Številka:
4
Journal Article
Recenzirano
Odprti dostop
Deploying neural networks (NNs) in low-resource domains is challenging because of their high computing, memory, and power requirements. For this reason, NNs are often quantized before deployment, but ...such an approach degrades their accuracy. Thus, we propose the counterexample-guided neural network quantization refinement (CEG4N) framework, which combines search-based quantization and equivalence checking. The former minimizes computational requirements, while the latter guarantees that the behavior of an NN does not change after quantization. We evaluate CEG4N on a diverse set of benchmarks, including large and small NNs. Our technique successfully quantizes the networks in the chosen evaluation set, while producing models with up to 163% better accuracy than state-of-the-art techniques.
The first attempts to apply the
k
-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic ...context-bounded model checker and uses an iterative deepening approach to verify, for each step
k
up to a given maximum, whether a given safety property
ϕ
holds in the program. The proposed
k
-induction algorithm consists of three different cases, called
base case
,
forward condition
, and
inductive step
. Intuitively, in the base case, we aim to find a counterexample with up to
k
loop unwindings; in the forward condition, we check whether loops have been fully unrolled and that
ϕ
holds in all states reachable within
k
unwindings; and in the inductive step, we check that whenever
ϕ
holds for
k
unwindings, it also holds after the next unwinding of the system. The algorithm was implemented in two different ways, a sequential and a parallel one, and the results were compared. Experimental results show that both forms of the algorithm can handle a wide variety of safety properties extracted from standard benchmarks, ranging from reachability to time constraints. And by comparison, the parallel algorithm solves more verification tasks in less time. This paper marks the first application of the
k
-induction algorithm to a broader range of C programs; in particular, we show that our
k
-induction method outperforms CPAChecker in terms of correct results, which is a state-of-the-art
k
-induction-based verification tool for C programs.
Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially with the number of ...program threads and statements. We propose and evaluate EBF (Ensembles of Bounded Model Checking with Fuzzing) - a technique that combines Bounded Model Checking (BMC) and Gray-Box Fuzzing (GBF) to find software vulnerabilities in concurrent programs. Since there are no publicly-available GBF tools for concurrent code, we first propose OpenGBF - a new open-source concurrency-aware gray-box fuzzer that explores different thread schedules by instrumenting the code under test with random delays. Then, we build an ensemble of a BMC tool and OpenGBF in the following way. On the one hand, when the BMC tool in the ensemble returns a counterexample, we use it as a seed for OpenGBF, thus increasing the likelihood of executing paths guarded by complex mathematical expressions. On the other hand, we aggregate the outcomes of the BMC and GBF tools in the ensemble using a decision matrix, thus improving the accuracy of EBF. We evaluate EBF against state-of-the-art pure BMC tools and show that it can generate up to 14.9% more correct verification witnesses than the corresponding BMC tools alone. Furthermore, we demonstrate the efficacy of OpenGBF, by showing that it can find 24.2% of the vulnerabilities in our evaluation suite, while non-concurrency-aware GBF tools can only find 0.55%. Finally, thanks to our concurrency-aware OpenGBF, EBF detects a data race in the open-source wolfMqtt library and reproduces known bugs in several other real-world programs, which demonstrates its effectiveness in finding vulnerabilities in real-world software.
ESBMC is an SMT-based bounded model checker that provides a bit-precise verification of both C and C++ programs. Bounded model checking (BMC) was developed to provide faster results when finding ...property violations; BMC achieves this by limiting the number of loop unwindings and recursion depth. The technique, however, is unable to prove correctness unless all loops and recursions are fully unwound, which might not be possible for some programs (e.g., infinite loops). The version of ESBMC described here is designed to avoid the problem of guessing the number of unwindings, which leads to a property violation; it incrementally verifies the program, searching only for property violations. Once ESBMC has found a property violation, it produces a test suite that contains at least one test to expose a bug. ESBMC can correctly produce 312 test cases, which are confirmed by the test validator employed by Test-Comp 2019.
DepthK is a source-to-source transformation tool that employs bounded model checking (BMC) to verify and falsify safety properties in single- and multi-threaded C programs, without manual annotation ...of loop invariants. Here, we describe and evaluate a proof-by-induction algorithm that combines
k
-induction with invariant inference to prove and refute safety properties. We apply two invariant generators to produce program invariants and feed these into a
k
-induction-based verification algorithm implemented in DepthK, which uses the efficient SMT-based context-bounded model checker (ESBMC) as sequential verification back-end. A set of C benchmarks from the International Competition on Software Verification (SV-COMP) and embedded-system applications extracted from the available literature are used to evaluate the effectiveness of the proposed approach. Experimental results show that
k
-induction with invariants can handle a wide variety of safety properties, in typical programs with loops and embedded software applications from the telecommunications, control systems, and medical domains. The results of our comparative evaluation extend the knowledge about approaches that rely on both BMC and
k
-induction for software verification, in the following ways. (1) The proposed method outperforms the existing implementations that use
k
-induction with an interval-invariant generator (
e.g.
, 2LS and ESBMC), in the category ConcurrencySafety, and overcame, in others categories, such as SoftwareSystems, other software verifiers that use plain BMC (
e.g.
, CBMC). Also, (2) it is more precise than other verifiers based on the property-directed reachability (PDR) algorithm (
i.e.
, SeaHorn, Vvt and CPAchecker-CTIGAR). This way, our methodology demonstrated improvement over existing BMC and
k
-induction-based approaches.
ESBMC 5.0: An Industrial-Strength C Model Checker Gadelha, Mikhail R.; Monteiro, Felipe R.; Morse, Jeremy ...
2018 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE),
2018-Sept.
Conference Proceeding
Odprti dostop
ESBMC is a mature, permissively licensed open-source context-bounded model checker for the verification of single- and multithreaded C programs. It can verify both predefined safety properties (e.g., ...bounds check, pointer safety, overflow) and user-defined program assertions automatically. ESBMC provides C++ and Python APIs to access internal data structures, allowing inspection and extension at any stage of the verification process. We discuss improvements over previous versions of ESBMC, including the description of new front- and back-ends, IEEE floating-point support, and an improved k-induction algorithm. A demonstration is available at https://www.youtube.com/watch?v=YcJjXHlN1v8.
PDF
