Biblio

Found 1589 results

Filters: Keyword is cryptography  [Clear All Filters]
2022-06-09
Aleksandrov, Mykyta.  2021.  Confirmation of Mutual Synchronization of the TPMs Using Hash Functions. 2021 IEEE 3rd International Conference on Advanced Trends in Information Theory (ATIT). :80–83.
This paper presents experimental results of evaluating the effect of network delay on the synchronization time of three parity machines. The possibility of using a hash function to confirm the synchronization of parity tree machines has been investigated. Three parity machines have been proposed as a modification of the symmetric encryption algorithm. One advantage of the method is the possibility to use the phenomenon of mutual synchronization of neural networks to generate an identical encryption key for users without the need to transfer it. As a result, the degree of influence of network delay and the type of hash function used on the synchronization time of neural networks was determined. The degree of influence of the network delay and hash function was determined experimentally. The hash function sha512 showed the best results. The tasks for further research have been defined.
Ambedkar, B. R., Bharti, P. K., Husain, Akhtar.  2021.  Design and Analysis of Hash Algorithm Using Autonomous Initial Value Proposed Secure Hash Algorithm64. 2021 IEEE 18th India Council International Conference (INDICON). :1–6.
A secure hash code or message authentication code is a one-way hash algorithm. It is producing a fixed-size hash function to be used to check verification, the integrity of electronic data, password storage. Numerous researchers have proposed hashing algorithms. They have a very high time complexity based on several steps, initial value, and key constants which are publically known. We are focusing here on the many exiting algorithms that are dependent on the initial value and key constant usage to increasing the security strength of the hash function which is publically known. Therefore, we are proposing autonomous initial value proposed secure hash algorithm (AIVPSHA64) in this research paper to produce sixty-four-bit secure hash code without the need of initial value and key constant, it is very useful for a smart card to verify their identity which has limited memory space. Then evaluate the performance of hash function using autonomous initial value proposed secure hash algorithm (AIVPSHA64) and will compare the result, which is found by python-3.9.0 programming language.
2022-05-12
Li, Fulin, Ji, Huifang, Zhou, Hongwei, Zhang, Chang.  2021.  A Dynamic and Secure Migration Method of Cryptographic Service Virtual Machine for Cloud Environment. 2021 7th International Conference on Computer and Communications (ICCC). :583–588.
In order to improve the continuity of cryptographic services and ensure the quality of services in the cloud environment, a dynamic migration framework of cryptographic service virtual machines based on the network shared storage system is proposed. Based on the study of the security threats in the migration process, a dynamic migration attack model is established, and the security requirement of dynamic migration is analyzed. It designs and implements the dynamic security migration management software, which includes a dynamic migration security enhancement module based on the Libvirt API, role-based access control policy, and transmission channel protection module. A cryptographic service virtual machine migration environment is built, and the designed management software and security mechanism are verified and tested. The experimental results show that the method proposed in the paper can effectively improve the security of cryptographic service virtual machine migration.
2022-07-01
Chen, Liquan, Guo, Xing, Lu, Tianyu, Gao, Yuan.  2021.  Formalization of the Secrecy Capacity in Non-degraded Wiretap Channel. 2021 7th International Conference on Computer and Communications (ICCC). :535–538.
Unlike the traditional key-exchange based cryptography, physical layer security is built on information theory and aims to achieve unconditional security by exploiting the physical characteristics of wireless channels. With the growth of the number of wireless devices, physical layer security has been gradually emphasized by researchers. Various physical layer security protocols have been proposed for different communication scenarios. Since these protocols are based on information-theoretic security and the formalization work for information theory were not complete when these protocols were proposed, the security of these protocols lacked formal proofs. In this paper, we propose a formal definition for the secrecy capacity in non-degraded wiretap channel model and a formal proof for the secrecy capacity in binary symmetric channel with the help of SSReflect/Coq theorem prover.
2022-10-20
Nahar, Nazmun, Ahmed, Md. Kawsher, Miah, Tareq, Alam, Shahriar, Rahman, Kh. Mustafizur, Rabbi, Md. Anayt.  2021.  Implementation of Android Based Text to Image Steganography Using 512-Bit Algorithm with LSB Technique. 2021 5th International Conference on Electrical Information and Communication Technology (EICT). :1—6.
Steganography security is the main concern in today’s informative world. The fact is that communication takes place to hide information secretly. Steganography is the technique of hiding secret data within an ordinary, non-secret, file, text message and images. This technique avoids detection of the secret data then extracted at its destination. The main reason for using steganography is, we can hide any secret message behind its ordinary file. This work presents a unique technique for image steganography based on a 512-bit algorithm. The secure stego image is a very challenging task to give protection. Therefore we used the least significant bit (LSB) techniques for implementing stego and cover image. However, data encryption and decryption are used to embedded text and replace data into the least significant bit (LSB) for better approaches. Android-based interface used in encryption-decryption techniques that evaluated in this process.Contribution—this research work with 512-bit data simultaneously in a block cipher to reduce the time complexity of a system, android platform used for data encryption decryption process. Steganography model works with stego image that interacts with LSB techniques for data hiding.
2022-05-12
Şengül, Özkan, Özkılıçaslan, Hasan, Arda, Emrecan, Yavanoğlu, Uraz, Dogru, Ibrahim Alper, Selçuk, Ali Aydın.  2021.  Implementing a Method for Docker Image Security. 2021 International Conference on Information Security and Cryptology (ISCTURKEY). :34–39.
Containers that can be easily created, transported and scaled with the use of container-based virtualization technologies work better than classical virtualization technologies and provide efficient resource usage. The Docker platform is one of the most widely used solutions among container-based virtualization technologies. The OS-level virtualization of the Docker platform and the container’s use of the host operating system kernel may cause security problems. In this study, a method including static and dynamic analysis has been proposed to ensure Docker image and container security. In the static analysis phase of the method, the packages of the images are scanned for vulnerabilities and malware. In the dynamic analysis phase, Docker containers are run for a certain period of time, after the open port scanning, network traffic is analyzed with the Snort3. Seven Docker images are analyzed and the results are shared.
2022-05-06
Bansal, Malti, Gupta, Shubham, Mathur, Siddhant.  2021.  Comparison of ECC and RSA Algorithm with DNA Encoding for IoT Security. 2021 6th International Conference on Inventive Computation Technologies (ICICT). :1340—1343.
IoT is still an emerging technology without a lot of standards around it, which makes it difficult to integrate it into existing businesses, what's more, with restricted assets and expanding gadgets that essentially work with touchy information. Thus, information safety has become urgent for coders and clients. Thus, painstakingly chosen and essentially tested encryption calculations should be utilized to grow the gadgets productively, to decrease the danger of leaking the delicate information. This investigation looks at the ECC calculation (Elliptic Curve Cryptography) and Rivest-Shamir-Adleman (RSA) calculation. Furthermore, adding the study of DNA encoding operation in DNA computing with ECC to avoid attackers from getting access to the valuable data.
2022-07-29
Butler, Martin, Butler, Rika.  2021.  The Influence of Mobile Operating Systems on User Security Behavior. 2021 IEEE 5th International Conference on Cryptography, Security and Privacy (CSP). :134—138.

Mobile security remains a concern for multiple stakeholders. Safe user behavior is crucial key to avoid and mitigate mobile threats. The research used a survey design to capture key constructs of mobile user threat avoidance behavior. Analysis revealed that there is no significant difference between the two key drivers of secure behavior, threat appraisal and coping appraisal, for Android and iOS users. However, statistically significant differences in avoidance motivation and avoidance behavior of users of the two operating systems were displayed. This indicates that existing threat avoidance models may be insufficient to comprehensively deal with factors that affect mobile user behavior. A newly introduced variable, perceived security, shows a difference in the perceptions of their level of protection among the users of the two operating systems, providing a new direction for research into mobile security.

2021-12-22
Malhotra, Diksha, Srivastava, Shubham, Saini, Poonam, Singh, Awadhesh Kumar.  2021.  Blockchain Based Audit Trailing of XAI Decisions: Storing on IPFS and Ethereum Blockchain. 2021 International Conference on COMmunication Systems NETworkS (COMSNETS). :1–5.
Explainable Artificial Intelligence (XAI) generates explanations which are used by regulators to audit the responsibility in case of any catastrophic failure. These explanations are currently stored in centralized systems. However, due to lack of security and traceability in centralized systems, the respective owner may temper the explanations for his convenience in order to avoid any penalty. Nowadays, Blockchain has emerged as one of the promising technologies that might overcome the security limitations. Hence, in this paper, we propose a novel Blockchain based framework for proof-of-authenticity pertaining to XAI decisions. The framework stores the explanations in InterPlanetary File System (IPFS) due to storage limitations of Ethereum Blockchain. Further, a Smart Contract is designed and deployed in order to supervise the storage and retrieval of explanations from Ethereum Blockchain. Furthermore, to induce cryptographic security in the network, an explanation's hash is calculated and stored in Blockchain too. Lastly, we perform the cost and security analysis of our proposed system.
2021-12-21
Xiaojian, Zhang, Liandong, Chen, Jie, Fan, Xiangqun, Wang, Qi, Wang.  2021.  Power IoT Security Protection Architecture Based on Zero Trust Framework. 2021 IEEE 5th International Conference on Cryptography, Security and Privacy (CSP). :166–170.
The construction of the power Internet of Things has led various terminals to access the corporate network on a large scale. The internal and external business interaction and data exchange are more extensive. The current security protection system is based on border isolation protection. This is difficult to meet the needs of the power Internet of Things connection and open shared services. This paper studies the application scheme of the ``zero trust'' typical business scenario of the power Internet of Things with ``Continuous Identity Authentication and Dynamic Access Control'' as the core, and designs the power internet security protection architecture based on zero trust.
2022-04-25
Hiraga, Hiroki, Nishi, Hiroaki.  2021.  Network Transparent Decrypting of Cryptographic Stream Considering Service Provision at the Edge. 2021 IEEE 19th International Conference on Industrial Informatics (INDIN). :1–6.
The spread of Internet of Things (IoT) devices and high-speed communications, such as 5G, makes their services rich and diverse. Therefore, it is desirable to perform functions of rich services transparently and use edge computing environments flexibly at intermediate locations on the Internet, from the perspective of a network system. When this type of edge computing environment is achieved, IoT nodes as end devices of the Internet can fully utilize edge computing systems and cloud systems without any change, such as switching destination IP addresses between them, along with protocol maintenance for the switching. However, when the data transfer in the communication is encrypted, a decryption method is necessary at the edge, to realize these transparent edge services. In this study, a transparent common key-exchanging method with cloud service has been proposed as the destination node of a communication pair, to transparently decrypt a secure sockets layer-encrypted communication stream at the edge area. This enables end devices to be free from any changes and updates to communicate with the destination node.
2021-12-21
Elumar, Eray Can, Sood, Mansi, Ya\u gan, Osman.  2021.  On the Connectivity and Giant Component Size of Random K-out Graphs Under Randomly Deleted Nodes. 2021 IEEE International Symposium on Information Theory (ISIT). :2572–2577.
Random K-out graphs, denoted \$$\backslash$mathbbH(n;K)\$, are generated by each of the \$n\$ nodes drawing \$K\$ out-edges towards \$K\$ distinct nodes selected uniformly at random, and then ignoring the orientation of the arcs. Recently, random K-out graphs have been used in applications as diverse as random (pairwise) key predistribution in ad-hoc networks, anonymous message routing in crypto-currency networks, and differentially-private federated averaging. In many applications, connectivity of the random K-out graph when some of its nodes are dishonest, have failed, or have been captured is of practical interest. We provide a comprehensive set of results on the connectivity and giant component size of \$$\backslash$mathbbH(n;K\_n,$\backslash$gamma\_n)\$, i.e., random K-out graph when \textsubscriptn of its nodes, selected uniformly at random, are deleted. First, we derive conditions for \textsubscriptn and \$n\$ that ensure, with high probability (whp), the connectivity of the remaining graph when the number of deleted nodes is \$$\backslash$gamma\_n=Ømega(n)\$ and \$$\backslash$gamma\_n=o(n)\$, respectively. Next, we derive conditions for \$$\backslash$mathbbH(n;K\_n, $\backslash$gamma\_n)\$ to have a giant component, i.e., a connected subgraph with \$Ømega(n)\$ nodes, whp. This is also done for different scalings of \textsubscriptn and upper bounds are provided for the number of nodes outside the giant component. Simulation results are presented to validate the usefulness of the results in the finite node regime.
Hamouid, Khaled, Omar, Mawloud, Adi, Kamel.  2021.  A Privacy-Preserving Authentication Model Based on Anonymous Certificates in IoT. 2021 Wireless Days (WD). :1–6.
This paper proposes an anonymity based mechanism for providing privacy in IoT environment. Proposed scheme allows IoT entities to anonymously interacting and authenticating with each other, or even proving that they have trustworthy relationship without disclosing their identities. Authentication is based on an anonymous certificates mechanism where interacting IoT entities could unlinkably prove possession of a valid certificate without revealing any incorporated identity-related information, thereby preserving their privacy and thwarting tracking and profiling attacks. Through a security analysis, we demonstrate the reliability of our solution.
2022-03-23
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.
2022-08-12
Basin, David, Lochbihler, Andreas, Maurer, Ueli, Sefidgar, S. Reza.  2021.  Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streamlined versions of simulation-based frameworks to cope with this complexity. Hence, a central question is how to abstract details from composability results and enable their formal verification.In this paper, we focus on the modeling of system communication in composable security statements. Existing formal models consider fixed communication patterns to reduce the complexity of their proofs. However, as we will show, this can affect the reusability of security statements. We propose an abstract approach to modeling system communication in Constructive Cryptography that avoids this problem. Our approach is suitable for mechanized verification and we use CryptHOL, a framework for developing mechanized cryptography proofs, to implement it in the Isabelle/HOL theorem prover. As a case study, we formalize the construction of a secure channel using Diffie-Hellman key exchange and a one-time-pad.
2021-12-20
Künnemann, Robert, Garg, Deepak, Backes, Michael.  2021.  Accountability in the Decentralised-Adversary Setting. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
A promising paradigm in protocol design is to hold parties accountable for misbehavior, instead of postulating that they are trustworthy. Recent approaches in defining this property, called accountability, characterized malicious behavior as a deviation from the protocol that causes a violation of the desired security property, but did so under the assumption that all deviating parties are controlled by a single, centralized adversary. In this work, we investigate the setting where multiple parties can deviate with or without coordination in a variant of the applied-π calculus.We first demonstrate that, under realistic assumptions, it is impossible to determine all misbehaving parties; however, we show that accountability can be relaxed to exclude causal dependencies that arise from the behavior of deviating parties, and not from the protocol as specified. We map out the design space for the relaxation, point out protocol classes separating these notions and define conditions under which we can guarantee fairness and completeness. Most importantly, we discover under which circumstances it is correct to consider accountability in the single-adversary setting, where this property can be verified with off-the-shelf protocol verification tools.
2022-06-09
Sujatha, G., Raj, Jeberson Retna.  2021.  Digital Data Identification for Deduplication Process using Cryptographic Hashing Techniques. 2021 International Conference on Intelligent Technologies (CONIT). :1–4.
The cloud storage system is a very big boon for the organizations and individuals who are all in the need of storage space to accommodate huge volume of digital data. The cloud storage space can handle various types of digital data like text, image, video and audio. Since the storage space can be shared among different users, it is possible to have duplicate copies of data in the storage space. An efficient mechanism is required to identify the digital data uniquely in order to check the duplicity. There are various ways by which the digital data can be identified. One among such technique is hash-based identification. Using cryptographic hashing algorithms, every data can be uniquely identified. The unique property of hashing algorithm helps to identify the data uniquely. In this research work, we are going to discuss the advantage of using cryptographic hashing algorithm for digital data identification and the comparison of various hashing algorithms.
2022-02-24
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.
Gondron, Sébastien, Mödersheim, Sebastian.  2021.  Vertical Composition and Sound Payload Abstraction for Stateful Protocols. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
This paper deals with a problem that arises in vertical composition of protocols, i.e., when a channel protocol is used to encrypt and transport arbitrary data from an application protocol that uses the channel. Our work proves that we can verify that the channel protocol ensures its security goals independent of a particular application. More in detail, we build a general paradigm to express vertical composition of an application protocol and a channel protocol, and we give a transformation of the channel protocol where the application payload messages are replaced by abstract constants in a particular way that is feasible for standard automated verification tools. We prove that this transformation is sound for a large class of channel and application protocols. The requirements that channel and application have to satisfy for the vertical composition are all of an easy-to-check syntactic nature.
2022-04-26
Wang, Luyao, Huang, Chunguang, Cheng, Hai.  2021.  Quantum attack-resistant signature scheme from lattice cryptography for WFH. 2021 IEEE 2nd International Conference on Big Data, Artificial Intelligence and Internet of Things Engineering (ICBAIE). :868–871.

With the emergence of quantum computers, traditional digital signature schemes based on problems such as large integer solutions and discrete logarithms will no longer be secure, and it is urgent to find effective digital signature schemes that can resist quantum attacks. Lattice cryptography has the advantages of computational simplicity and high security. In this paper, we propose an identity-based digital signature scheme based on the rejection sampling algorithm. Unlike most schemes that use a common Gaussian distribution, this paper uses a bimodal Gaussian distribution, which improves efficiency. The identity-based signature scheme is more convenient for practical application than the traditional certificate-based signature scheme.

2021-12-20
Piccolboni, Luca, Guglielmo, Giuseppe Di, Carloni, Luca P., Sethumadhavan, Simha.  2021.  CRYLOGGER: Detecting Crypto Misuses Dynamically. 2021 IEEE Symposium on Security and Privacy (SP). :1972–1989.
Cryptographic (crypto) algorithms are the essential ingredients of all secure systems: crypto hash functions and encryption algorithms, for example, can guarantee properties such as integrity and confidentiality. Developers, however, can misuse the application programming interfaces (API) of such algorithms by using constant keys and weak passwords. This paper presents CRYLOGGER, the first open-source tool to detect crypto misuses dynamically. CRYLOGGER logs the parameters that are passed to the crypto APIs during the execution and checks their legitimacy offline by using a list of crypto rules. We compared CRYLOGGER with CryptoGuard, one of the most effective static tools to detect crypto misuses. We show that our tool complements the results of CryptoGuard, making the case for combining static and dynamic approaches. We analyzed 1780 popular Android apps downloaded from the Google Play Store to show that CRYLOGGER can detect crypto misuses on thousands of apps dynamically and automatically. We reverse-engineered 28 Android apps and confirmed the issues flagged by CRYLOGGER. We also disclosed the most critical vulnerabilities to app developers and collected their feedback.
2022-05-06
S, Sudersan, B, Sowmiya, V.S, Abhijith, M, Thangavel, P, Varalakshmi.  2021.  Enhanced DNA Cryptosystem for Secure Cloud Data Storage. 2021 2nd International Conference on Secure Cyber Computing and Communications (ICSCCC). :337—342.
Cloud computing has revolutionized the way how users store, process, and use data. It has evolved over the years to put forward various sophisticated models that offer enhanced performance. The growth of electronic data stored in the Cloud has made it crucial to access data without data loss and leakage. Security threats still prevent significant corporations that use sensitive data to employ cloud computing to handle their data. Traditional cryptographic techniques like DES, AES, etc... provide data confidentiality but are computationally complex. To overcome such complexities, a unique field of cryptography known as DNA Cryptography came into existence. DNA cryptography is a new field of cryptography that utilizes the chemical properties of DNA for secure data encoding. DNA cryptographic algorithms are much faster than traditional cryptographic methods and can bring about greater security with lesser computational costs. In this paper, we have proposed an enhanced DNA cryptosystem involving operations such as encryption, encoding table generation, and decryption based on the chemical properties of DNA. The performance analysis has proven that the proposed DNA cryptosystem is secure and efficient in Cloud data storage.
2022-07-13
Liu, Xian.  2021.  A Primitive Cipher with Machine Learning. 2021 IEEE International Black Sea Conference on Communications and Networking (BlackSeaCom). :1—6.
Multi-access edge computing (MEC) equipped with artificial intelligence is a promising technology in B5G wireless systems. Due to outsourcing and other transactions, some primitive security modules need to be introduced. In this paper, we design a primitive cipher based on double discrete exponentiation and double discrete logarithm. The machine learning methodology is incorporated in the development. Several interesting results are obtained. It reveals that the number of key-rounds is critically important.
2022-05-12
Li, Shih-Wei, Li, Xupeng, Gu, Ronghui, Nieh, Jason, Zhuang Hui, John.  2021.  A Secure and Formally Verified Linux KVM Hypervisor. 2021 IEEE Symposium on Security and Privacy (SP). :1782–1799.

Commodity hypervisors are widely deployed to support virtual machines (VMs) on multiprocessor hardware. Their growing complexity poses a security risk. To enable formal verification over such a large codebase, we introduce microverification, a new approach that decomposes a commodity hypervisor into a small core and a set of untrusted services so that we can prove security properties of the entire hypervisor by verifying the core alone. To verify the multiprocessor hypervisor core, we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification, and the top layer specification is refined by all layers of the core implementation. To verify commodity hypervisor features that require dynamically changing information flow, we introduce data oracles to mask intentional information flow. We can then prove noninterference at the top layer specification and guarantee the resulting security properties hold for the entire hypervisor implementation. Using microverification, we retrofitted the Linux KVM hypervisor with only modest modifications to its codebase. Using Coq, we proved that the hypervisor protects the confidentiality and integrity of VM data, while retaining KVM’s functionality and performance. Our work is the first machine-checked security proof for a commodity multiprocessor hypervisor.

Morbitzer, Mathias, Proskurin, Sergej, Radev, Martin, Dorfhuber, Marko, Salas, Erick Quintanar.  2021.  SEVerity: Code Injection Attacks against Encrypted Virtual Machines. 2021 IEEE Security and Privacy Workshops (SPW). :444–455.

Modern enterprises increasingly take advantage of cloud infrastructures. Yet, outsourcing code and data into the cloud requires enterprises to trust cloud providers not to meddle with their data. To reduce the level of trust towards cloud providers, AMD has introduced Secure Encrypted Virtualization (SEV). By encrypting Virtual Machines (VMs), SEV aims to ensure data confidentiality, despite a compromised or curious Hypervisor. The SEV Encrypted State (SEV-ES) extension additionally protects the VM’s register state from unauthorized access. Yet, both extensions do not provide integrity of the VM’s memory, which has already been abused to leak the protected data or to alter the VM’s control-flow. In this paper, we introduce the SEVerity attack; a missing puzzle piece in the series of attacks against the AMD SEV family. Specifically, we abuse the system’s lack of memory integrity protection to inject and execute arbitrary code within SEV-ES-protected VMs. Contrary to previous code execution attacks against the AMD SEV family, SEVerity neither relies on a specific CPU version nor on any code gadgets inside the VM. Instead, SEVerity abuses the fact that SEV-ES prohibits direct memory access into the encrypted memory. Specifically, SEVerity injects arbitrary code into the encrypted VM through I/O channels and uses the Hypervisor to locate and trigger the execution of the encrypted payload. This allows us to sidestep the protection mechanisms of SEV-ES. Overall, our results demonstrate a success rate of 100% and hence highlight that memory integrity protection is an obligation when encrypting VMs. Consequently, our work presents the final stroke in a series of attacks against AMD SEV and SEV-ES and renders the present implementation as incapable of protecting against a curious, vulnerable, or malicious Hypervisor.