Visible to the public Biblio

Filters: Keyword is model checking  [Clear All Filters]
2021-10-12
He, Leifeng, Liu, Guanjun.  2020.  Petri Nets Based Verification of Epistemic Logic and Its Application on Protocols of Privacy and Security. 2020 IEEE World Congress on Services (SERVICES). :25–28.
Epistemic logic can specify many design requirements of privacy and security of multi-agent systems (MAS). The existing model checkers of epistemic logic use some programming languages to describe MAS, induce Kripke models as the behavioral representation of MAS, apply Ordered Binary Decision Diagrams (OBDD) to encode Kripke models to solve their state explosion problem and verify epistemic logic based on the encoded Kripke models. However, these programming languages are usually non-intuitive. More seriously, their OBDD-based model checking processes are often time-consuming due to their dynamic variable ordering for OBDD. Therefore, we define Knowledge-oriented Petri Nets (KPN) to intuitively describe MAS, induce similar reachability graphs as the behavioral representation of KPN, apply OBDD to encode all reachable states, and finally verify epistemic logic. Although we also use OBDD, we adopt a heuristic method for the computation of a static variable order instead of dynamic variable ordering. More importantly, while verifying an epistemic formula, we dynamically generate its needed similar relations, which makes our model checking process much more efficient. In this paper, we introduce our work.
2021-10-04
Zheng, Xiaoyu, Liu, Dongmei, Zhu, Hong, Bayley, Ian.  2020.  Pattern-Based Approach to Modelling and Verifying System Security. 2020 IEEE International Conference on Service Oriented Systems Engineering (SOSE). :92–102.
Security is one of the most important problems in the engineering of online service-oriented systems. The current best practice in security design is a pattern-oriented approach. A large number of security design patterns have been identified, categorised and documented in the literature. The design of a security solution for a system starts with identification of security requirements and selection of appropriate security design patterns; these are then composed together. It is crucial to verify that the composition of security design patterns is valid in the sense that it preserves the features, semantics and soundness of the patterns and correct in the sense that the security requirements are met by the design. This paper proposes a methodology that employs the algebraic specification language SOFIA to specify security design patterns and their compositions. The specifications are then translated into the Alloy formalism and their validity and correctness are verified using the Alloy model checker. A tool that translates SOFIA into Alloy is presented. A case study with the method and the tool is also reported.
2021-09-30
Wang, Guoqing, Zhuang, Lei, Liu, Taotao, Li, Shuxia, Yang, Sijin, Lan, Julong.  2020.  Formal Analysis and Verification of Industrial Control System Security via Timed Automata. 2020 International Conference on Internet of Things and Intelligent Applications (ITIA). :1–5.
The industrial Internet of Things (IIoT) can facilitate industrial upgrading, intelligent manufacturing, and lean production. Industrial control system (ICS) is a vital support mechanism for many key infrastructures in the IIoT. However, natural defects in the ICS network security mechanism and the susceptibility of the programmable logic controller (PLC) program to malicious attack pose a threat to the safety of national infrastructure equipment. To improve the security of the underlying equipment in ICS, a model checking method based on timed automata is proposed in this work, which can effectively model the control process and accurately simulate the system state when incorporating time factors. Formal analysis of the ICS and PLC is then conducted to formulate malware detection rules which can constrain the normal behavior of the system. The model checking tool UPPAAL is then used to verify the properties by detecting whether there is an exception in the system and determine the behavior of malware through counter-examples. The chemical reaction control system in Tennessee-Eastman process is taken as an example to carry out modeling, characterization, and verification, and can effectively detect multiple patterns of malware and propose relevant security policy recommendations.
2021-08-02
Abdul Basit Ur Rahim, Muhammad, Duan, Qi, Al-Shaer, Ehab.  2020.  A Formal Analysis of Moving Target Defense. 2020 IEEE 44th Annual Computers, Software, and Applications Conference (COMPSAC). :1802—1807.
Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology.
2021-01-25
Ghazo, A. T. Al, Ibrahim, M., Ren, H., Kumar, R..  2020.  A2G2V: Automatic Attack Graph Generation and Visualization and Its Applications to Computer and SCADA Networks. IEEE Transactions on Systems, Man, and Cybernetics: Systems. 50:3488–3498.
Securing cyber-physical systems (CPS) and Internet of Things (IoT) systems requires the identification of how interdependence among existing atomic vulnerabilities may be exploited by an adversary to stitch together an attack that can compromise the system. Therefore, accurate attack graphs play a significant role in systems security. A manual construction of the attack graphs is tedious and error-prone, this paper proposes a model-checking-based automated attack graph generator and visualizer (A2G2V). The proposed A2G2V algorithm uses existing model-checking tools, an architecture description tool, and our own code to generate an attack graph that enumerates the set of all possible sequences in which atomic-level vulnerabilities can be exploited to compromise system security. The architecture description tool captures a formal representation of the networked system, its atomic vulnerabilities, their pre-and post-conditions, and security property of interest. A model-checker is employed to automatically identify an attack sequence in the form of a counterexample. Our own code integrated with the model-checker parses the counterexamples, encodes those for specification relaxation, and iterates until all attack sequences are revealed. Finally, a visualization tool has also been incorporated with A2G2V to generate a graphical representation of the generated attack graph. The results are illustrated through application to computer as well as control (SCADA) networks.
2020-10-16
Babenko, Liudmila, Pisarev, Ilya.  2018.  Security Analysis of the Electronic Voting Protocol Based on Blind Intermediaries Using the SPIN Verifier. 2018 International Conference on Cyber-Enabled Distributed Computing and Knowledge Discovery (CyberC). :43—435.

Cryptographic protocols are the basis for the security of any protected system, including the electronic voting system. One of the most effective ways to analyze protocol security is to use verifiers. In this paper, the formal verifier SPIN was used to analyze the security of the cryptographic protocol for e-voting, which is based on model checking using linear temporal logic (LTL). The cryptographic protocol of electronic voting is described. The main structural units of the Promela language used for simulation in the SPIN verifier are described. The model of the electronic voting protocol in the language Promela is given. The interacting parties, transferred data, the order of the messages transmitted between the parties are described. Security of the cryptographic protocol using the SPIN tool is verified. The simulation of the protocol with active intruder using the man in the middle attack (MITM) to substitute data is made. In the simulation results it is established that the protocol correctly handles the case of an active attack on the parties' authentication.

2020-09-28
Chen, Yuqi, Poskitt, Christopher M., Sun, Jun.  2018.  Learning from Mutants: Using Code Mutation to Learn and Monitor Invariants of a Cyber-Physical System. 2018 IEEE Symposium on Security and Privacy (SP). :648–660.
Cyber-physical systems (CPS) consist of sensors, actuators, and controllers all communicating over a network; if any subset becomes compromised, an attacker could cause significant damage. With access to data logs and a model of the CPS, the physical effects of an attack could potentially be detected before any damage is done. Manually building a model that is accurate enough in practice, however, is extremely difficult. In this paper, we propose a novel approach for constructing models of CPS automatically, by applying supervised machine learning to data traces obtained after systematically seeding their software components with faults ("mutants"). We demonstrate the efficacy of this approach on the simulator of a real-world water purification plant, presenting a framework that automatically generates mutants, collects data traces, and learns an SVM-based model. Using cross-validation and statistical model checking, we show that the learnt model characterises an invariant physical property of the system. Furthermore, we demonstrate the usefulness of the invariant by subjecting the system to 55 network and code-modification attacks, and showing that it can detect 85% of them from the data logs generated at runtime.
2020-09-21
Fang, Zheng, Fu, Hao, Gu, Tianbo, Qian, Zhiyun, Jaeger, Trent, Mohapatra, Prasant.  2019.  ForeSee: A Cross-Layer Vulnerability Detection Framework for the Internet of Things. 2019 IEEE 16th International Conference on Mobile Ad Hoc and Sensor Systems (MASS). :236–244.
The exponential growth of Internet-of-Things (IoT) devices not only brings convenience but also poses numerous challenging safety and security issues. IoT devices are distributed, highly heterogeneous, and more importantly, directly interact with the physical environment. In IoT systems, the bugs in device firmware, the defects in network protocols, and the design flaws in system configurations all may lead to catastrophic accidents, causing severe threats to people's lives and properties. The challenge gets even more escalated as the possible attacks may be chained together in a long sequence across multiple layers, rendering the current vulnerability analysis inapplicable. In this paper, we present ForeSee, a cross-layer formal framework to comprehensively unveil the vulnerabilities in IoT systems. ForeSee generates a novel attack graph that depicts all of the essential components in IoT, from low-level physical surroundings to high-level decision-making processes. The corresponding graph-based analysis then enables ForeSee to precisely capture potential attack paths. An optimization algorithm is further introduced to reduce the computational complexity of our analysis. The illustrative case studies show that our multilayer modeling can capture threats ignored by the previous approaches.
2020-05-15
Sepulveda, Johanna, Aboul-Hassan, Damian, Sigl, Georg, Becker, Bernd, Sauer, Matthias.  2018.  Towards the formal verification of security properties of a Network-on-Chip router. 2018 IEEE 23rd European Test Symposium (ETS). :1—6.
pubcrawl, Network on Chip Security, Scalability, resiliency, resilience, metrics, Vulnerabilities and design flaws in Network-on-Chip (NoC) routers can be exploited in order to spy, modify and constraint the sensitive communication inside the Multi-Processors Systems-on-Chip (MPSoCs). Although previous works address the NoC threat, finding secure and efficient solutions to verify the security is still a challenge. In this work, we propose for the first time a method to formally verify the correctness and the security properties of a NoC router in order to provide the proper communication functionality and to avoid NoC attacks. We present a generalized verification flow that proves a wide set of implementation-independent security-related properties to hold. We employ unbounded model checking techniques to account for the highly-sequential behaviour of the NoC systems. The evaluation results demonstrate the feasibility of our approach by presenting verification results of six different NoC routing architectures demonstrating the vulnerabilities of each design.
2020-03-16
Chondamrongkul, Nacha, Sun, Jing, Wei, Bingyang, Warren, Ian.  2019.  Parallel Verification of Software Architecture Design. 2019 IEEE 19th International Symposium on High Assurance Systems Engineering (HASE). :50–57.
In the component-based software system, certain behaviours of components and their composition may affect system reliability at runtime. This problem can be early detected through the automated verification of software architecture design, by which model checking is one of the techniques to achieve this. However, its practicality and performance issue remain challenges. This paper presents a scalable approach for the software architecture verification. The modelling is proposed to manifest the behaviours in the software component, in order to detect problematic behaviours, such as circular dependency and performance bottleneck. The outcome of the verification identifies the problem and the scenarios that cause it. In order to mitigate the verification performance issue, the parallelism is applied to the verification process so that multiple decomposed models can be simultaneously verified on a multi-threaded environment. As some software systems are designed as the monolithic architecture, we present a method that helps to automatically decompose a large monolithic model into a set of smaller sub-models. Our approach was evaluated and proved to enhance the performance of the verification process for the large-scale complex software systems.
Gajavelly, Raj Kumar, Baumgartner, Jason, Ivrii, Alexander, Kanzelman, Robert L., Ghosh, Shiladitya.  2019.  Input Elimination Transformations for Scalable Verification and Trace Reconstruction. 2019 Formal Methods in Computer Aided Design (FMCAD). :10–18.
We present two novel sound and complete netlist transformations, which substantially improve verification scalability while enabling very efficient trace reconstruction. First, we present a 2QBF variant of input reparameterization, capable of eliminating inputs without introducing new logic and without complete range computation. While weaker in reduction potential, it yields up to 4 orders of magnitude speedup to trace reconstruction when used as a fast-and-lossy preprocess to traditional reparameterization. Second, we present a novel scalable approach to leverage sequential unateness to merge selective inputs, in cases greatly reducing netlist size and verification complexity. Extensive benchmarking demonstrates the utility of these techniques. Connectivity verification particularly benefits from these reductions, up to 99.8%.
Mercaldo, Francesco, Martinelli, Fabio, Santone, Antonella.  2019.  Real-Time SCADA Attack Detection by Means of Formal Methods. 2019 IEEE 28th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). :231–236.
SCADA control systems use programmable logic controller to interface with critical machines. SCADA systems are used in critical infrastructures, for instance, to control smart grid, oil pipelines, water distribution and chemical manufacturing plants: an attacker taking control of a SCADA system could cause various damages, both to the infrastructure but also to people (for instance, adding chemical substances into a water distribution systems). In this paper we propose a method to detect attacks targeting SCADA systems. We exploit model checking, in detail we model logs from SCADA systems into a network of timed automata and, through timed temporal logic, we characterize the behaviour of a SCADA system under attack. Experiments performed on a SCADA water distribution system confirmed the effectiveness of the proposed method.
2020-02-17
Letychevskyi, Oleksandr.  2019.  Two-Level Algebraic Method for Detection of Vulnerabilities in Binary Code. 2019 10th IEEE International Conference on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS). 2:1074–1077.
This study introduces formal methods for detection of vulnerabilities in binary code. It considers the transformation of binary code into behavior algebra expressions and formalization of vulnerabilities. The detection method has two levels: behavior matching and symbolic execution with vulnerability pattern matching. This enables more efficient performance.
2020-02-10
Todorov, Vassil, Taha, Safouan, Boulanger, Frédéric, Hernandez, Armando.  2019.  Improved Invariant Generation for Industrial Software Model Checking of Time Properties. 2019 IEEE 19th International Conference on Software Quality, Reliability and Security (QRS). :334–341.
Modern automotive embedded software is mostly designed using model-based design tools such as Simulink or SCADE, and source code is generated automatically from the models. Formal proof using symbolic model checking has been integrated in these tools and can provide a higher assurance by proving safety-critical properties. Our experience shows that proving properties involving time is rather challenging when they involve long durations and timers. These properties are generally not inductive and even advanced techniques such as PDR/IC3 are unable to handle them on production models in reasonable time. In this paper, we first present our industrial use case and comment on the results obtained with the existing model checkers. Then we present our invariant generator and methodology for selecting invariants according to physical dimensions. They enable the proof of properties with long-running timers. Finally, we discuss their implementation and benchmarks.
2020-01-21
Tran-Jørgensen, Peter W. V., Kulik, Tomas, Boudjadar, Jalil, Larsen, Peter Gorm.  2019.  Security Analysis of Cloud-Connected Industrial Control Systems Using Combinatorial Testing. Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design. :1–11.

Industrial control systems are moving from monolithic to distributed and cloud-connected architectures, which increases system complexity and vulnerability, thus complicates security analysis. When exhaustive verification accounts for this complexity the state space being sought grows drastically as the system model evolves and more details are considered. Eventually this may lead to state space explosion, which makes exhaustive verification infeasible. To address this, we use VDM-SL's combinatorial testing feature to generate security attacks that are executed against the model to verify whether the system has the desired security properties. We demonstrate our approach using a cloud-connected industrial control system that is responsible for performing safety-critical tasks and handling client requests sent to the control network. Although the approach is not exhaustive it enables verification of mitigation strategies for a large number of attacks and complex systems within reasonable time.

2019-12-11
Zhao, Jianfeng.  2018.  Case Study: Discovering Hardware Trojans Based on Model Checking. Proceedings of the 8th International Conference on Communication and Network Security. :64–68.

Hardware Trojan may cause changes in system functions, system information leakage, and system damage or system paralysis. According to the hardware Trojan classification method, this paper discusses the hardware Trojan that belongs to the design stage, the behavior level description, the internal trigger, and it changes the function of processor, it is a hardware Trojan of combinational logic. The domestic and foreign research institutions put forward a variety of methods for the detection of hardware Trojans. In this paper, based on the open source processor OR1200 RTL source code, Aiming at a kind of hardware Trojan, which is composed of combinational logic trigger, one of the formal methods, the model checking technique, is used to detect the hardware Trojan. The experiment uses the open source EBMC model detection tool, uses the RTL source code as the model input, and uses SVA to describe the property input. The experimental results show that the model checking technique can be used as an effective hardware Trojan detection method.

2019-06-28
Chen, G., Wang, D., Li, T., Zhang, C., Gu, M., Sun, J..  2018.  Scalable Verification Framework for C Program. 2018 25th Asia-Pacific Software Engineering Conference (APSEC). :129-138.

Software verification has been well applied in safety critical areas and has shown the ability to provide better quality assurance for modern software. However, as lines of code and complexity of software systems increase, the scalability of verification becomes a challenge. In this paper, we present an automatic software verification framework TSV to address the scalability issues: (i) the extended structural abstraction and property-guided program slicing to solve large-scale program verification problem, saving time and memory without losing accuracy; (ii) automatically select different verification methods according to the program and property context to improve the verification efficiency. For evaluation, we compare TSV's different configurations with existing C program verifiers based on open benchmarks. We found that TSV with auto-selection performs better than with bounded model checking only or with extended structural abstraction only. Compared to existing tools such as CMBC and CPAChecker, it acquires 10%-20% improvement of accuracy and 50%-90% improvement of memory consumption.

2019-05-09
Shrestha, Roshan, Mehrpouyan, Hoda, Xu, Dianxiang.  2018.  Model Checking of Security Properties in Industrial Control Systems (ICS). Proceedings of the Eighth ACM Conference on Data and Application Security and Privacy. :164-166.

With the increasing inter-connection of operation technology to the IT network, the security threat to the Industrial Control System (ICS) is increasing daily. Therefore, it is critical to utilize formal verification technique such as model checking to mathematically prove the correctness of security and safety requirements in the controller logic before it is deployed on the field. However, model checking requires considerable effort for regular ICS users and control technician to verify properties. This paper, provides a simpler approach to the model checking of temperature process control system by first starting with the control module design without formal verification. Second, identifying possible vulnerabilities in such design. Third, verifying the safety and security properties with a formal method. 

2019-05-01
Mili, S., Nguyen, N., Chelouah, R..  2018.  Attack Modeling and Verification for Connected System Security. 2018 13th Annual Conference on System of Systems Engineering (SoSE). :157–162.

In the development process of critical systems, one of the main challenges is to provide early system validation and verification against vulnerabilities in order to reduce cost caused by late error detection. We propose in this paper an approach that, firstly allows formally describe system security specifications, thanks to our suggested extended attack tree. Secondly, static and dynamic system modeling by using a SysML connectivity profile to model error propagation is introduced. Finally, a model checker has been used in order to validate system specifications.

2019-02-08
Yi, F., Cai, H. Y., Xin, F. Z..  2018.  A Logic-Based Attack Graph for Analyzing Network Security Risk Against Potential Attack. 2018 IEEE International Conference on Networking, Architecture and Storage (NAS). :1-4.
In this paper, we present LAPA, a framework for automatically analyzing network security risk and generating attack graph for potential attack. The key novelty in our work is that we represent the properties of networks and zero day vulnerabilities, and use logical reasoning algorithm to generate potential attack path to determine if the attacker can exploit these vulnerabilities. In order to demonstrate the efficacy, we have implemented the LAPA framework and compared with three previous network vulnerability analysis methods. Our analysis results have a low rate of false negatives and less cost of processing time due to the worst case assumption and logical property specification and reasoning. We have also conducted a detailed study of the efficiency for generation attack graph with different value of attack path number, attack path depth and network size, which affect the processing time mostly. We estimate that LAPA can produce high quality results for a large portion of networks.
2018-05-24
Joshaghani, R., Mehrpouyan, H..  2017.  A Model-Checking Approach for Enforcing Purpose-Based Privacy Policies. 2017 IEEE Symposium on Privacy-Aware Computing (PAC). :178–179.

With the growth of Internet in many different aspects of life, users are required to share private information more than ever. Hence, users need a privacy management tool that can enforce complex and customized privacy policies. In this paper, we propose a privacy management system that not only allows users to define complex privacy policies for data sharing actions, but also monitors users' behavior and relationships to generate realistic policies. In addition, the proposed system utilizes formal modeling and model-checking approach to prove that information disclosures are valid and privacy policies are consistent with one another.

2018-05-09
Abate, Alessandro.  2017.  Formal Verification of Complex Systems: Model-Based and Data-Driven Methods. Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design. :91–93.

Two known shortcomings of standard techniques in formal verification are the limited capability to provide system-level assertions, and the scalability to large, complex models, such as those needed in Cyber-Physical Systems (CPS) applications. Leveraging data, which nowadays is becoming ever more accessible, has the potential to mitigate such limitations. However, this leads to a lack of formal proofs that are needed for modern safety-critical systems. This contribution presents a research initiative that addresses these shortcomings by bringing model-based techniques and data-driven methods together, which can help pushing the envelope of existing algorithms and tools in formal verification and thus expanding their applicability to complex engineering systems, such as CPS. In the first part of the contribution, we discuss a new, formal, measurement-driven and model-based automated technique, for the quantitative verification of physical systems with partly unknown dynamics. We formulate this setup as a data-driven Bayesian inference problem, formally embedded within a quantitative, model-based verification procedure. We argue that the approach can be applied to complex physical systems that are key for CPS applications, dealing with spatially continuous variables, evolving under complex dynamics, driven by external inputs, and accessed under noisy measurements. In the second part of the contribution, we concentrate on systems represented by models that evolve under probabilistic and heterogeneous (continuous/discrete - that is "hybrid" - as well as nonlinear) dynamics. Such stochastic hybrid models (also known as SHS) are a natural mathematical framework for CPS. With focus on model-based verification procedures, we provide algorithms for quantitative model checking of temporal specifications on SHS with formal guarantees. This is attained via the development of formal abstraction techniques that are based on quantitative approximations. Theory is complemented by algorithms, all packaged in software tools that are available to users, and which are applied here in the domain of Smart Energy.

Hamouda, R. Ben, Hafaiedh, I. Ben.  2017.  Formal Modeling and Verification of a Wireless Body Area Network (WBAN) Protocol: S-TDMA Protocol. 2017 International Conference on Internet of Things, Embedded Systems and Communications (IINTEC). :72–77.

WBANs integrate wearable and implanted devices with wireless communication and information processing systems to monitor the well-being of an individual. Various MAC (Medium Access Control) protocols with different objectives have been proposed for WBANs. The fact that any flaw in these critical systems may lead to the loss of one's life implies that testing and verifying MAC's protocols for such systems are on the higher level of importance. In this paper, we firstly propose a high-level formal and scalable model with timing aspects for a MAC protocol particularly designed for WBANs, named S-TDMA (Statistical frame based TDMA protocol). The protocol uses TDMA (Time Division Multiple Access) bus arbitration, which requires temporal aspect modeling. Secondly, we propose a formal validation of several relevant properties such as deadlock freedom, fairness and mutual exclusion of this protocol at a high level of abstraction. The protocol was modeled using a composition of timed automata components, and verification was performed using a real-time model checker.

2018-03-05
Schnepf, N., Badonnel, R., Lahmadi, A., Merz, S..  2017.  Automated Verification of Security Chains in Software-Defined Networks with Synaptic. 2017 IEEE Conference on Network Softwarization (NetSoft). :1–9.

Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.

Schnepf, N., Badonnel, R., Lahmadi, A., Merz, S..  2017.  Automated Verification of Security Chains in Software-Defined Networks with Synaptic. 2017 IEEE Conference on Network Softwarization (NetSoft). :1–9.
Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.