Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Survey of Practical Formal Methods for Security
208
0
0.0
(
0
)
Added by
Tomas Kulik
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
In todays world, critical infrastructure is often controlled by computing systems. This introduces new risks for cyber attacks, which can compromise the security and disrupt the functionality of these systems. It is therefore necessary to build such systems with strong guarantees of resiliency against cyber attacks. One way to achieve this level of assurance is using formal verification, which provides proofs of system compliance with desired cyber security properties. The use of Formal Methods (FM) in aspects of cyber security and safety-critical systems are reviewed in this article. We split FM into the three main classes: theorem proving, model checking and lightweight FM. To allow the different uses of FM to be compared, we define a common set of terms. We further develop categories based on the type of computing system FM are applied in. Solutions in each class and category are presented, discussed, compared and summarised. We describe historical highlights and developments and present a state-of-the-art review in the area of FM in cyber security. This review is presented from the point of view of FM practitioners and researchers, commenting on the trends in each of the classes and categories. This is achieved by considering all types of FM, several types of security and safety critical systems and by structuring the taxonomy accordingly. The article hence provides a comprehensive overview of FM and techniques available to system designers of security-critical systems, simplifying the process of choosing the right tool for the task. The article concludes by summarising the discussion of the review, focusing on best practices, challenges, general future trends and directions of research within this field.
rate research
Read More
While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.
The rapid involution of the mobile generation with incipient data networking capabilities and utilization has exponentially increased the data traffic volumes. Such traffic drains various key issues in 5G mobile backhaul networks. Security of mobile backhaul is of utmost importance; however, there are a limited number of articles, which have explored such a requirement. This paper discusses the potential design issues and key challenges of the secure 5G mobile backhaul architecture. The comparisons of the existing state-of-the-art solutions for secure mobile backhaul, together with their major contributions have been explored. Furthermore, the paper discussed various key issues related to Quality of Service (QoS), routing and scheduling, resource management, capacity enhancement, latency, security-management, and handovers using mechanisms like Software Defined Networking and millimeter Wave technologies. Moreover, the trails of research challenges and future directions are additionally presented.
Quantum key distribution (QKD) gradually has become a crucial element of practical secure communication. In different scenarios, the security analysis of genuine QKD systems is complicated. A universal secret key rate calculation method, used for realistic factors such as multiple degrees of freedom encoding, asymmetric protocol structures, equipment flaws, environmental noise, and so on, is still lacking. Based on the correlations of statistical data, we propose a security analysis method without restriction on encoding schemes. This method makes a trade-off between applicability and accuracy, which can effectively analyze various existing QKD systems. We illustrate its ability by analyzing source flaws and a high-dimensional asymmetric protocol. Results imply that our method can give tighter bounds than the Gottesman-Lo-Lutkenhaus-Preskill (GLLP) analysis and is beneficial to analyze protocols with complex encoding structures. Our work has the potential to become a reference standard for the security analysis of practical QKD.
Industrial automation systems (IAS) need to be highly dependable; they should not merely function as expected but also do so in a reliable, safe, and secure manner. Formal methods are mathematical techniques that can greatly aid in developing dependable systems and can be used across all phases of the system development life cycle (SDLC), including requirements engineering, system design and implementation, verification and validation (testing), maintenance, and even documentation. This state-of-the-art survey reports existing formal approaches for creating more dependable IAS, focusing on static formal methods that are used before a system is completely implemented. We categorize surveyed works based on the phases of the SDLC, allowing us to identify research gaps and promising future directions for each phase.
The use of deep neural networks (DNNs) in safety-critical applications like mobile health and autonomous driving is challenging due to numerous model-inherent shortcomings. These shortcomings are diverse and range from a lack of generalization over insufficient interpretability to problems with malicious inputs. Cyber-physical systems employing DNNs are therefore likely to suffer from safety concerns. In recent years, a zoo of state-of-the-art techniques aiming to address these safety concerns has emerged. This work provides a structured and broad overview of them. We first identify categories of insufficiencies to then describe research activities aiming at their detection, quantification, or mitigation. Our paper addresses both machine learning experts and safety engineers: The former ones might profit from the broad range of machine learning topics covered and discussions on limitations of recent methods. The latter ones might gain insights into the specifics of modern ML methods. We moreover hope that our contribution fuels discussions on desiderata for ML systems and strategies on how to propel existing approaches accordingly.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
