TY  - JOUR
A1  - Lorenz, Claas
A1  - Clemens, Vera Elisabeth
A1  - Schrötter, Max
A1  - Schnor, Bettina
T1  - Continuous verification of network security compliance
JF  - IEEE transactions on network and service management
N2  - Continuous verification of network security compliance is an accepted need. Especially, the analysis of stateful packet filters plays a central role for network security in practice. But the few existing tools which support the analysis of stateful packet filters are based on general applicable formal methods like Satifiability Modulo Theories (SMT) or theorem prover and show runtimes in the order of minutes to hours making them unsuitable for continuous compliance verification. In this work, we address these challenges and present the concept of state shell interweaving to transform a stateful firewall rule set into a stateless rule set. This allows us to reuse any fast domain specific engine from the field of data plane verification tools leveraging smart, very fast, and domain specialized data structures and algorithms including Header Space Analysis (HSA). First, we introduce the formal language FPL that enables a high-level human-understandable specification of the desired state of network security. Second, we demonstrate the instantiation of a compliance process using a verification framework that analyzes the configuration of complex networks and devices - including stateful firewalls - for compliance with FPL policies. Our evaluation results show the scalability of the presented approach for the well known Internet2 and Stanford benchmarks as well as for large firewall rule sets where it outscales state-of-the-art tools by a factor of over 41.
KW  - Security
KW  - Tools
KW  - Network security
KW  - Engines
KW  - Benchmark testing;
KW  - Analytical models
KW  - Scalability
KW  - Network
KW  - security
KW  - compliance
KW  - formal
KW  - verification
Y1  - 2021
U6  - https://doi.org/10.1109/TNSM.2021.3130290
SN  - 1932-4537
VL  - 19
IS  - 2
SP  - 1729
EP  - 1745
PB  - Institute of Electrical and Electronics Engineers
CY  - New York
ER  - 
TY  - JOUR
A1  - Breitenreiter, Anselm
A1  - Andjelković, Marko
A1  - Schrape, Oliver
A1  - Krstić, Miloš
T1  - Fast error propagation probability estimates by answer set programming and approximate model counting
JF  - IEEE Access
N2  - We present a method employing Answer Set Programming in combination with Approximate Model Counting for fast and accurate calculation of error propagation probabilities in digital circuits. By an efficient problem encoding, we achieve an input data format similar to a Verilog netlist so that extensive preprocessing is avoided. By a tight interconnection of our application with the underlying solver, we avoid iterating over fault sites and reduce calls to the solver. Several circuits were analyzed with varying numbers of considered cycles and different degrees of approximation. Our experiments show, that the runtime can be reduced by approximation by a factor of 91, whereas the error compared to the exact result is below 1%.
KW  - Circuit faults
KW  - Integrated circuit modeling
KW  - Programming
KW  - Analytical models
KW  - Search problems
KW  - Flip-flops
KW  - Encoding
KW  - Answer set programming
KW  - approximate model counting
KW  - error propagation
KW  - radhard design
KW  - reliability analysis
KW  - selective fault tolerance
KW  - single event upsets
Y1  - 2022
U6  - https://doi.org/10.1109/ACCESS.2022.3174564
SN  - 2169-3536
VL  - 10
SP  - 51814
EP  - 51825
PB  - Inst. of Electr. and Electronics Engineers
CY  - Piscataway
ER  -