Visible to the public Biblio

Found 721 results

Filters: Keyword is Computational modeling  [Clear All Filters]
2022-04-01
Rezaei, Ghazal, Hashemi, Massoud Reza.  2021.  An SDN-based Firewall for Networks with Varying Security Requirements. 2021 26th International Computer Conference, Computer Society of Iran (CSICC). :1–7.
With the new coronavirus crisis, medical devices' workload has increased dramatically, leaving them growingly vulnerable to security threats and in need of a comprehensive solution. In this work, we take advantage of the flexible and highly manageable nature of Software Defined Networks (SDN) to design a thoroughgoing security framework that covers a health organization's various security requirements. Our solution comes to be an advanced SDN firewall that solves the issues facing traditional firewalls. It enables the partitioning of the organization's network and the enforcement of different filtering and monitoring behaviors on each partition depending on security conditions. We pursued the network's efficient and dynamic security management with the least human intervention in designing our model which makes it generally qualified to use in networks with different security requirements.
2022-03-23
Kayalvizhy, V., Banumathi, A..  2021.  A Survey on Cyber Security Attacks and Countermeasures in Smart Grid Metering Network. 2021 5th International Conference on Computing Methodologies and Communication (ICCMC). :160—165.
Smart grid (SG) network is one of the recently improved networks of tangled entities, objects, and smart metering infrastructure (SMI). It plays a vital part in sensing, acquiring, observing, aggregating, controlling, and dealing with various kinds of fields in SG. The SMI or advanced metering infrastructure (AMI) is proposed to make available a real-time transmissions connection among users and services are Time of use (TOU), Real time pricing (RTP), Critical Peak Pricing (CPP). In adding to, additional benefit of SMs is which are capable to report back to the service control center in near real time nontechnical losses (for instance, tampering with meters, bypassing meters, and illicit tapping into distribution systems). SMI supports two-way transmission meters reading electrical utilization at superior frequency. This data is treated in real time and signals send to manage demand. This paper expresses a transitory impression of cyberattack instances in customary energy networks and SMI. This paper presents cyber security attacks and countermeasures in Smart Grid Metering Network (SGMN). Based on the existing survey threat models, a number of proposed ways have been planned to deal with all threats in the formulation of the secrecy and privacy necessities of SG measurement network.
Shukla, Saurabh, Thakur, Subhasis, Breslin, John G..  2021.  Secure Communication in Smart Meters using Elliptic Curve Cryptography and Digital Signature Algorithm. 2021 IEEE International Conference on Cyber Security and Resilience (CSR). :261—266.
With the advancement in the growth of Internet-of-Things (IoT), its number of applications has also increased such as in healthcare, smart cities, vehicles, industries, household appliances, and Smart Grids (SG). One of the major applications of IoT is the SG and smart meter which consists of a large number of internet-connected sensors and can communicate bi-directionally in real-time. The SG network involves smart meters, data collectors, generators, and sensors connected with the internet. SG networks involve the generation, distribution, transmission, and consumption of electrical power supplies. It consists of Household Area Network (HAN), and Neighborhood Area Network (NAN) for communication. Smart meters can communicate bidirectionally with consumers and provide real-time information to utility offices. But this communication channel is a wide-open network for data transmission. Therefore, it makes the SG network and smart meter vulnerable to outside hacker and various Cyber-Physical System (CPS) attacks such as False Data Injection (FDI), inserting malicious data, erroneous data, manipulating the sensor reading values. Here cryptography techniques can play a major role along with the private blockchain model for secure data transmission in smart meters. Hence, to overcome these existing issues and challenges in smart meter communication we have proposed a blockchain-based system model for secure communication along with a novel Advanced Elliptic Curve Cryptography Digital Signature (AECCDS) algorithm in Fog Computing (FC) environment. Here FC nodes will work as miners at the edge of smart meters for secure and real-time communication. The algorithm is implemented using iFogSim, Geth version 1.9.25, Ganache, Truffle for compiling smart contracts, Anaconda (Python editor), and ATOM as language editor for the smart contracts.
Khlobystova, Anastasiia O., Abramov, Maxim V..  2021.  Adaptation of the Multi-pass social Engineering Attack Model Taking into Account Informational Influence. 2021 XXIV International Conference on Soft Computing and Measurements (SCM). :49–51.
One of the measures to prevent multi-pass social engineering attacks is to identify the chains of user, which are most susceptible to such attacks. The aim of the study is to combine a mathematical model for estimating the probability of success of the propagation of a multi-pass social engineering attack between users with a model for calculating information influence. Namely, it is proposed to include in estimating the intensity of interactions between users (which used in the model of the propagation of a multi-pass social engineering attack) estimating of power of influence actions of agents. The scientific significance of the work consists in the development of a mathematical structure for modeling the actions of an attacker-social engineer and creating a foundation for the subsequent analysis of the social graph of the organization's employees. The practical significance lies in the formation of opportunities for decision-makers. Therefore, they will be able to take more precise measures for increase the level of security as individual employees as the organization generally.
2022-03-22
Xu, Ben, Liu, Jun.  2021.  False Data Detection Based On LSTM Network In Smart Grid. 2021 4th International Conference on Advanced Electronic Materials, Computers and Software Engineering (AEMCSE). :314—317.
In contrast to traditional grids, smart grids can help utilities save energy, thereby reducing operating costs. In the smart grid, the quality of monitoring and control can be fully improved by combining computing and intelligent communication knowledge. However, this will expose the system to FDI attacks, and the system is vulnerable to intrusion. Therefore, it is very important to detect such erroneous data injection attacks and provide an algorithm to protect the system from such attacks. In this paper, a FDI detection method based on LSTM has been proposed, which is validated by the simulation on the ieee-14 bus platform.
Meng, Yu, Liangliang, Zhu, Yao, Rao, Yongxian, Yi, Jiaji, Liu.  2021.  Research on Fast Encryption Method for Smart Energy Management System in Smart Gird. 2021 International Conference on Communications, Information System and Computer Engineering (CISCE). :76—80.
Smart energy management system in smart grid carries a large number of sensitive data, which needs encryption algorithm to ensure the security of system communication. At present, most of the terminal devices of smart grid are embedded devices with limited computing resources, and their communication encryption mostly relies on AES encryption algorithm. It is difficult in key management and key distribution. Therefore, this paper proposes an improved ECC-AES hybrid encryption algorithm. Firstly, ECC algorithm is improved to improve the speed of encryption and decryption, and then the improved ECC algorithm is used as a supplement to AES algorithm. ECC is used to encrypt the AES key, which improves the security of the algorithm. At the same time, the experimental simulation also proves that the improved ECC algorithm has obvious performance improvement in computing time, CPU occupancy and memory usage.
Jiang, Xin, Yang, Qifan, Ji, Wen, Chen, Yanshu, Cai, Yuxiang, Li, Xiaoming.  2021.  Smart grid data security storage strategy based on cloud computing platform. 2021 6th International Conference on Smart Grid and Electrical Automation (ICSGEA). :69—74.
Aiming at the security problems of traditional smart grid data security storage strategy, this paper proposes a smart grid data security storage strategy based on cloud computing platform. Based on the analysis of cloud computing and cloud storage, the security storage of smart grid data is modeled to improve the security storage performance of power system. The dynamic key mechanism is introduced to obtain the initial key information in the key chain and generate the dynamic secret key. The hyperchaotic system is used to obtain the modified bit plane code in the key chain to form the context and decision of data storage. MQ arithmetic encoder is used for entropy coding to generate the corresponding data storage compressed code stream, and the smart grid data storage key is improved. Combined with encryption processing and decryption processing, the secure storage of smart grid data is realized. The experimental results show that the smart grid data security storage strategy based on cloud computing platform increases the security of smart grid data storage.
2022-03-15
Naik Sapavath, Naveen, Muhati, Eric, Rawat, Danda B..  2021.  Prediction and Detection of Cyberattacks using AI Model in Virtualized Wireless Networks. 2021 8th IEEE International Conference on Cyber Security and Cloud Computing (CSCloud)/2021 7th IEEE International Conference on Edge Computing and Scalable Cloud (EdgeCom). :97—102.
Securing communication between any two wireless devices or users is challenging without compromising sensitive/personal data. To address this problem, we have developed an artificial intelligence (AI) algorithm to secure communication on virtualized wireless networks. To detect cyberattacks in a virtualized environment is challenging compared to traditional wireless networks setting. However, we successfully investigate an efficient cyberattack detection algorithm using an AI algorithm in a Bayesian learning model for detecting cyberattacks on the fly. We have studied the results of Random Forest and deep neural network (DNN) models to detect the cyberattacks on a virtualized wireless network, having considered the required transmission power as a threshold value to classify suspicious activities in our model. We present both formal mathematical analysis and numerical results to support our claims. The numerical results show our accuracy in detecting cyberattacks in the proposed Bayesian model is better than Random Forest and DNN models. We have also compared both models in terms of detection errors. The performance comparison results show our proposed approach outperforms existing approaches in detection accuracy, precision, and recall.
Haowei, Liang, Chunyan, Hou, Jinsong, Wang, Chen, Chen.  2021.  Software Safety Verification Framework based on Predicate Abstraction. 2021 IEEE 45th Annual Computers, Software, and Applications Conference (COMPSAC). :1327—1332.
Program verification techniques have gained increasing popularity in academic and industrial circles during the last years. Predicate abstraction is a traditional and practical verification technique, which can solve the problem of state space explosion pretty well. Many software verification tools have implemented it. But these implementations are not user-friendly, or scalable. Aimed at these problems, we describe and implement a new automatic predicate abstraction framework, CChecker, for proving the safety of procedural programs with integer assignments. CChecker is a whole system composed of two parts: front and back end. The front end preprocesses and parses the source programs into logic models based on Clang. And the back end resolves the models based on Z3 to get software safety property. At last, the experiments show the potential of CChecker.
2022-03-14
Hahanov, V.I., Saprykin, A.S..  2021.  Federated Machine Learning Architecture for Searching Malware. 2021 IEEE East-West Design Test Symposium (EWDTS). :1—4.
Modern technologies for searching viruses, cloud-edge computing, and also federated algorithms and machine learning architectures are shown. The architectures for searching malware based on the xor metric applied in the design and test of computing systems are proposed. A Federated ML method is proposed for searching for malware, which significantly speeds up learning without the private big data of users. A federated infrastructure of cloud-edge computing is described. The use of signature analysis and the assertion engine for searching malware is shown. The paradigm of LTF-computing for searching destructive components in software applications is proposed.
Gustafson, Erik, Holzman, Burt, Kowalkowski, James, Lamm, Henry, Li, Andy C. Y., Perdue, Gabriel, Isakov, Sergei V., Martin, Orion, Thomson, Ross, Beall, Jackson et al..  2021.  Large scale multi-node simulations of ℤ2 gauge theory quantum circuits using Google Cloud Platform. 2021 IEEE/ACM Second International Workshop on Quantum Computing Software (QCS). :72—79.
Simulating quantum field theories on a quantum computer is one of the most exciting fundamental physics applications of quantum information science. Dynamical time evolution of quantum fields is a challenge that is beyond the capabilities of classical computing, but it can teach us important lessons about the fundamental fabric of space and time. Whether we may answer scientific questions of interest using near-term quantum computing hardware is an open question that requires a detailed simulation study of quantum noise. Here we present a large scale simulation study powered by a multi-node implementation of qsim using the Google Cloud Platform. We additionally employ newly-developed GPU capabilities in qsim and show how Tensor Processing Units — Application-specific Integrated Circuits (ASICs) specialized for Machine Learning — may be used to dramatically speed up the simulation of large quantum circuits. We demonstrate the use of high performance cloud computing for simulating ℤ2 quantum field theories on system sizes up to 36 qubits. We find this lattice size is not able to simulate our problem and observable combination with sufficient accuracy, implying more challenging observables of interest for this theory are likely beyond the reach of classical computation using exact circuit simulation.
2022-03-10
Tiwari, Sarthak, Bansal, Ajay.  2021.  Domain-Agnostic Context-Aware Framework for Natural Language Interface in a Task-Based Environment. 2021 IEEE 45th Annual Computers, Software, and Applications Conference (COMPSAC). :15—20.
Smart home assistants are becoming a norm due to their ease-of-use. They employ spoken language as an interface, facilitating easy interaction with their users. Even with their obvious advantages, natural-language based interfaces are not prevalent outside the domain of home assistants. It is hard to adopt them for computer-controlled systems due to the numerous complexities involved with their implementation in varying fields. The main challenge is the grounding of natural language base terms into the underlying system's primitives. The existing systems that do use natural language interfaces are specific to one problem domain only.In this paper, a domain-agnostic framework that creates natural language interfaces for computer-controlled systems has been developed by creating a customizable mapping between the language constructs and the system primitives. The framework employs ontologies built using OWL (Web Ontology Language) for knowledge representation and machine learning models for language processing tasks.
2022-03-09
Ahmadi, Fardin, Sonia, Gupta, Gaurav, Zahra, Syed Rameem, Baglat, Preeti, Thakur, Puja.  2021.  Multi-factor Biometric Authentication Approach for Fog Computing to ensure Security Perspective. 2021 8th International Conference on Computing for Sustainable Global Development (INDIACom). :172—176.
Cloud Computing is a technology which provides flexibility through scalability. Like, Cloud computing, nowadays, Fog computing is considered more revolutionary and dynamic technology. But the main problem with the Fog computing is to take care of its security as in this also person identification is done by single Sign-In system. To come out from the security problem raised in Fog computing, an innovative approach has been suggested here. In the present paper, an approach has been proposed that combines different biometric techniques to verify the authenticity of a person and provides a complete model that will be able to provide a necessary level of verification and security in fog computing. In this model, several biometric techniques have been used and each one of them individually helps extract out more authentic and detailed information after every step. Further, in the presented paper, different techniques and methodologies have been examined to assess the usefulness of proposed technology in reducing the security threats. The paper delivers a capacious technique for biometric authentication for bolstering the fog security.
2022-03-01
Wang, Xingbin, Zhao, Boyan, HOU, RUI, Awad, Amro, Tian, Zhihong, Meng, Dan.  2021.  NASGuard: A Novel Accelerator Architecture for Robust Neural Architecture Search (NAS) Networks. 2021 ACM/IEEE 48th Annual International Symposium on Computer Architecture (ISCA). :776–789.
Due to the wide deployment of deep learning applications in safety-critical systems, robust and secure execution of deep learning workloads is imperative. Adversarial examples, where the inputs are carefully designed to mislead the machine learning model is among the most challenging attacks to detect and defeat. The most dominant approach for defending against adversarial examples is to systematically create a network architecture that is sufficiently robust. Neural Architecture Search (NAS) has been heavily used as the de facto approach to design robust neural network models, by using the accuracy of detecting adversarial examples as a key metric of the neural network's robustness. While NAS has been proven effective in improving the robustness (and accuracy in general), the NAS-generated network models run noticeably slower on typical DNN accelerators than the hand-crafted networks, mainly because DNN accelerators are not optimized for robust NAS-generated models. In particular, the inherent multi-branch nature of NAS-generated networks causes unacceptable performance and energy overheads.To bridge the gap between the robustness and performance efficiency of deep learning applications, we need to rethink the design of AI accelerators to enable efficient execution of robust (auto-generated) neural networks. In this paper, we propose a novel hardware architecture, NASGuard, which enables efficient inference of robust NAS networks. NASGuard leverages a heuristic multi-branch mapping model to improve the efficiency of the underlying computing resources. Moreover, NASGuard addresses the load imbalance problem between the computation and memory-access tasks from multi-branch parallel computing. Finally, we propose a topology-aware performance prediction model for data prefetching, to fully exploit the temporal and spatial localities of robust NAS-generated architectures. We have implemented NASGuard with Verilog RTL. The evaluation results show that NASGuard achieves an average speedup of 1.74× over the baseline DNN accelerator.
Chen, Shuyu, Li, Wei, Liu, Jun, Jin, Haoyu, Yin, Xuehui.  2021.  Network Intrusion Detection Based on Subspace Clustering and BP Neural Network. 2021 8th IEEE International Conference on Cyber Security and Cloud Computing (CSCloud)/2021 7th IEEE International Conference on Edge Computing and Scalable Cloud (EdgeCom). :65–70.
This paper proposes a novel network intrusion detection algorithm based on the combination of Subspace Clustering (SSC) and BP neural network. Firstly, we perform a subspace clustering algorithm on the network data set to obtain different subspaces. Secondly, BP neural network intrusion detection is carried out on the data in different subspaces, and calculate the prediction error value. By comparing with the pre-set accuracy, the threshold is constantly updated to improve the ability to identify network attacks. By comparing with K-means, DBSCAN, SSC-EA and k-KNN intrusion detection model, the SSC-BP neural network model can detect the most attacked networks with the lowest false detection rate.
Zhao, Ruijie, Li, Zhaojie, Xue, Zhi, Ohtsuki, Tomoaki, Gui, Guan.  2021.  A Novel Approach Based on Lightweight Deep Neural Network for Network Intrusion Detection. 2021 IEEE Wireless Communications and Networking Conference (WCNC). :1–6.
With the ubiquitous network applications and the continuous development of network attack technology, all social circles have paid close attention to the cyberspace security. Intrusion detection systems (IDS) plays a very important role in ensuring computer and communication systems security. Recently, deep learning has achieved a great success in the field of intrusion detection. However, the high computational complexity poses a major hurdle for the practical deployment of DL-based models. In this paper, we propose a novel approach based on a lightweight deep neural network (LNN) for IDS. We design a lightweight unit that can fully extract data features while reducing the computational burden by expanding and compressing feature maps. In addition, we use inverse residual structure and channel shuffle operation to achieve more effective training. Experiment results show that our proposed model for intrusion detection not only reduces the computational cost by 61.99% and the model size by 58.84%, but also achieves satisfactory accuracy and detection rate.
Jingyi, Wu, Xusheng, Gan, Jieli, Huang, Shenghou, Li.  2021.  ELM Network Intrusion Detection Model Based on SLPP Feature Extraction. 2021 IEEE International Conference on Power, Intelligent Computing and Systems (ICPICS). :46–49.
To improve the safety precaution level of network system, a combined network intrusion detection method is proposed based on Supervised Locality Preserving Projections (SLPP) feature extraction and Extreme Learning Machine (ELM). In this method, the feature extraction capability of SLPP is first used to reduce the dimensionality of the original network connection and system audit data, and get a feature set, then, based on this, the advantages of ELM in pattern recognition is adopted to build a network intrusion detection model for detecting and determining intrusion behavior. Simulation results show that, under the same experiment conditions, compared with traditional neural networks and support vector machines, the proposed method has more advantages in training efficiency and generalization performance.
2022-02-25
Xie, Bing, Tan, Zilong, Carns, Philip, Chase, Jeff, Harms, Kevin, Lofstead, Jay, Oral, Sarp, Vazhkudai, Sudharshan S., Wang, Feiyi.  2021.  Interpreting Write Performance of Supercomputer I/O Systems with Regression Models. 2021 IEEE International Parallel and Distributed Processing Symposium (IPDPS). :557—566.

This work seeks to advance the state of the art in HPC I/O performance analysis and interpretation. In particular, we demonstrate effective techniques to: (1) model output performance in the presence of I/O interference from production loads; (2) build features from write patterns and key parameters of the system architecture and configurations; (3) employ suitable machine learning algorithms to improve model accuracy. We train models with five popular regression algorithms and conduct experiments on two distinct production HPC platforms. We find that the lasso and random forest models predict output performance with high accuracy on both of the target systems. We also explore use of the models to guide adaptation in I/O middleware systems, and show potential for improvements of at least 15% from model-guided adaptation on 70% of samples, and improvements up to 10 x on some samples for both of the target systems.

2022-02-24
Dax, Alexander, Künnemann, Robert.  2021.  On the Soundness of Infrastructure Adversaries. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
Campus Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation. In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols.We show, in general, how the soundness and completeness of a rule-based model can be ensured by verifying trace properties, linking soundness to safety properties and completeness to liveness properties. We then demonstrate the approach for a recently proposed threat model that quantifies the confidentiality of email communication on the Internet, including DNS, DNSSEC, and SMTP. Using off-the-shelf protocol verification tools, we discover two flaws in their threat model. After fixing them, we show that it provides symbolic soundness.
Wang, Haoyu.  2021.  Compression Optimization For Automatic Verification of Network Configuration. 2021 6th International Conference on Intelligent Computing and Signal Processing (ICSP). :1409–1412.
In the era of big data and artificial intelligence, computer networks have become an important infrastructure, and the Internet has become ubiquitous. The most basic property of computer networks is reachability. The needs of the modern Internet mainly include cost, performance, reliability, and security. However, even for experienced network engineers, it is very difficult to manually conFigure the network to meet the needs of the modern large-scale Internet. The engineers often make mistakes, which can cause network paralysis, resulting in incalculable losses. Due to the development of automatic reasoning technology, automatic verification of network configuration is used to avoid mistakes. Network verification is at least an NP-C problem, so it is necessary to compress the network to reduce the network scale, thereby reducing the network verification time. This paper proposes a new model of network modeling, which is more suitable for the verification of network configuration on common protocols (such as RIP, BGP). On the basis of the existing compression method, two compression rules are added to compress the modeled network, reducing network verification time and conducting network reachability verification experiments on common networks. The experimental results are slightly better than the current compression methods.
Baelde, David, Delaune, Stéphanie, Jacomme, Charlie, Koutsos, Adrien, Moreau, Solène.  2021.  An Interactive Prover for Protocol Verification in the Computational Model. 2021 IEEE Symposium on Security and Privacy (SP). :537–554.
Given the central importance of designing secure protocols, providing solid mathematical foundations and computer-assisted methods to attest for their correctness is becoming crucial. Here, we elaborate on the formal approach introduced by Bana and Comon in [10], [11], which was originally designed to analyze protocols for a fixed number of sessions, and lacks support for proof mechanization.In this paper, we present a framework and an interactive prover allowing to mechanize proofs of security protocols for an arbitrary number of sessions in the computational model. More specifically, we develop a meta-logic as well as a proof system for deriving security properties. Proofs in our system only deal with high-level, symbolic representations of protocol executions, similar to proofs in the symbolic model, but providing security guarantees at the computational level. We have implemented our approach within a new interactive prover, the Squirrel prover, taking as input protocols specified in the applied pi-calculus, and we have performed a number of case studies covering a variety of primitives (hashes, encryption, signatures, Diffie-Hellman exponentiation) and security properties (authentication, strong secrecy, unlinkability).
Hess, Andreas V., Mödersheim, Sebastian, Brucker, Achim D., Schlichtkrull, Anders.  2021.  Performing Security Proofs of Stateful Protocols. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step towards achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results such as soundness of a typed model
Barthe, Gilles, Blazy, Sandrine, Hutin, Rémi, Pichardie, David.  2021.  Secure Compilation of Constant-Resource Programs. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–12.
Observational non-interference (ONI) is a generic information-flow policy for side-channel leakage. Informally, a program is ONI-secure if observing program leakage during execution does not reveal any information about secrets. Formally, ONI is parametrized by a leakage function l, and different instances of ONI can be recovered through different instantiations of l. One popular instance of ONI is the cryptographic constant-time (CCT) policy, which is widely used in cryptographic libraries to protect against timing and cache attacks. Informally, a program is CCT-secure if it does not branch on secrets and does not perform secret-dependent memory accesses. Another instance of ONI is the constant-resource (CR) policy, a relaxation of the CCT policy which is used in Amazon's s2n implementation of TLS and in several other security applications. Informally, a program is CR-secure if its cost (modelled by a tick operator over an arbitrary semi-group) does not depend on secrets.In this paper, we consider the problem of preserving ONI by compilation. Prior work on the preservation of the CCT policy develops proof techniques for showing that main compiler optimisations preserve the CCT policy. However, these proof techniques critically rely on the fact that the semi-group used for modelling leakage satisfies the property: l1+ l1' = l2+l2'$\Rightarrow$l1=l2$\wedge$ l1' = l2' Unfortunately, this non-cancelling property fails for the CR policy, because its underlying semi-group is ($\backslash$mathbbN, +) and it is currently not known how to extend existing techniques to policies that do not satisfy non-cancellation.We propose a methodology for proving the preservation of the CR policy during a program transformation. We present an implementation of some elementary compiler passes, and apply the methodology to prove the preservation of these passes. Our results have been mechanically verified using the Coq proof assistant.
Yu, Miao, Gligor, Virgil, Jia, Limin.  2021.  An I/O Separation Model for Formal Verification of Kernel Implementations. 2021 IEEE Symposium on Security and Privacy (SP). :572–589.

Commodity I/O hardware often fails to separate I/O transfers of isolated OS and applications code. Even when using the best I/O hardware, commodity systems sometimes trade off separation assurance for increased performance. Remarkably, device firmware need not be malicious. Instead, any malicious driver, even if isolated in its own execution domain, can manipulate its device to breach I/O separation. To prevent such vulnerabilities with high assurance, a formal I/O separation model and its use in automatic generation of secure I/O kernel code is necessary.This paper presents a formal I/O separation model, which defines a separation policy based on authorization of I/O transfers and is hardware agnostic. The model, its refinement, and instantiation in the Wimpy kernel design, are formally specified and verified in Dafny. We then specify the kernel implementation and automatically generate verified-correct assembly code that enforces the I/O separation policies. Our formal modeling enables the discovery of heretofore unknown design and implementation vulnerabilities of the original Wimpy kernel. Finally, we outline how the model can be applied to other I/O kernels and conclude with the key lessons learned.

2022-02-22
Mingyang, Qiu, Qingwei, Meng, Yan, Fu, Xikang, Wang.  2021.  Analysis of Zero-Day Virus Suppression Strategy based on Moving Target Defense. 2021 IEEE International Conference on Signal Processing, Communications and Computing (ICSPCC). :1—4.
In order to suppress the spread of zero-day virus in the network effectively, a zero-day virus suppression strategy was proposed. Based on the mechanism of zero-day virus transmission and the idea of platform dynamic defense, the corresponding methods of virus transmission suppression are put forward. By changing the platform switching frequency, the scale of zero-day virus transmission and its inhibition effect are simulated in a small-world network model. Theory and computer simulation results show that the idea of platform switching can effectively restrain the spread of virus.