Visible to the public Biblio

Found 1732 results

Filters: Keyword is security  [Clear All Filters]
2020-03-27
Jadidi, Mahya Soleimani, Zaborski, Mariusz, Kidney, Brian, Anderson, Jonathan.  2019.  CapExec: Towards Transparently-Sandboxed Services. 2019 15th International Conference on Network and Service Management (CNSM). :1–5.
Network services are among the riskiest programs executed by production systems. Such services execute large quantities of complex code and process data from arbitrary — and untrusted — network sources, often with high levels of system privilege. It is desirable to confine system services to a least-privileged environment so that the potential damage from a malicious attacker can be limited, but existing mechanisms for sandboxing services require invasive and system-specific code changes and are insufficient to confine broad classes of network services. Rather than sandboxing one service at a time, we propose that the best place to add sandboxing to network services is in the service manager that starts those services. As a first step towards this vision, we propose CapExec, a process supervisor that can execute a single service within a sandbox based on a service declaration file in which, required resources whose limited access to are supported by Caper services, are specified. Using the Capsicum compartmentalization framework and its Casper service framework, CapExec provides robust application sandboxing without requiring any modifications to the application itself. We believe that this is the first step towards ubiquitous sandboxing of network services without the costs of virtualization.
Liu, Wenqing, Zhang, Kun, Tu, Bibo, Lin, Kunli.  2019.  HyperPS: A Hypervisor Monitoring Approach Based on Privilege Separation. 2019 IEEE 21st International Conference on High Performance Computing and Communications; IEEE 17th International Conference on Smart City; IEEE 5th International Conference on Data Science and Systems (HPCC/SmartCity/DSS). :981–988.
In monolithic operating system (OS), any error of system software can be exploit to destroy the whole system. The situation becomes much more severe in cloud environment, when the kernel and the hypervisor share the same address space. The security of guest Virtual Machines (VMs), both sensitive data and vital code, can no longer be guaranteed, once the hypervisor is compromised. Therefore, it is essential to deploy some security approaches to secure VMs, regardless of the hypervisor is safe or not. Some approaches propose microhypervisor reducing attack surface, or a new software requiring a higher privilege level than hypervisor. In this paper, we propose a novel approach, named HyperPS, which separates the fundamental and crucial privilege into a new trusted environment in order to monitor hypervisor. A pivotal condition for HyperPS is that hypervisor must not be allowed to manipulate any security-sensitive system resources, such as page tables, system control registers, interaction between VM and hypervisor as well as VM memory mapping. Besides, HyperPS proposes a trusted environment which does not rely on any higher privilege than the hypervisor. We have implemented a prototype for KVM hypervisor on x86 platform with multiple VMs running Linux. KVM with HyperPS can be applied to current commercial cloud computing industry with portability. The security analysis shows that this approach can provide effective monitoring against attacks, and the performance evaluation confirms the efficiency of HyperPS.
Boehm, Barry, Rosenberg, Doug, Siegel, Neil.  2019.  Critical Quality Factors for Rapid, Scalable, Agile Development. 2019 IEEE 19th International Conference on Software Quality, Reliability and Security Companion (QRS-C). :514–515.
Agile methods frequently have difficulties with qualities, often specifying quality requirements as stories, e.g., "As a user, I need a safe and secure system." Such projects will generally schedule some capability releases followed by safety and security releases, only to discover user-developer misunderstandings and unsecurable agile code, leading to project failure. Very large agile projects also have further difficulties with project velocity and scalability. Examples are trying to use daily standup meetings, 2-week sprints, shared tacit knowledge vs. documents, and dealing with user-developer misunderstandings. At USC, our Parallel Agile, Executable Architecture research project shows some success at mid-scale (50 developers). We also examined several large (hundreds of developers) TRW projects that had succeeded with rapid, high-quality development. The paper elaborates on their common Critical Quality Factors: a concurrent 3-team approach, an empowered Keeper of the Project Vision, and a management approach emphasizing qualities.
Lai, Chengzhe, Ding, Yuhan.  2019.  A Secure Blockchain-Based Group Mobility Management Scheme in VANETs. 2019 IEEE/CIC International Conference on Communications in China (ICCC). :340–345.
Vehicular Ad-hoc Network (VANET) can provide vehicle to vehicle (V2V) and vehicle to infrastructure (V2I) communications for efficient and safe transportation. The vehicles features high mobility, thus undergoing frequent handovers when they are moving, which introduces the significant overload on the network entities. To address the problem, the distributed mobility management (DMM) protocol for next generation mobile network has been proposed, which can be well combined with VANETs. Although the existing DMM solutions can guarantee the smooth handovers of vehicles, the security has not been fully considered in the mobility management. Moreover, the most of existing schemes cannot support group communication scenario. In this paper, we propose an efficient and secure group mobility management scheme based on the blockchain. Specifically, to reduce the handover latency and signaling cost during authentication, aggregate message authentication code (AMAC) and one-time password (OTP) are adopted. The security analysis and the performance evaluation results show that the proposed scheme can not only enhance the security functionalities but also support fast handover authentication.
2020-03-23
Rathore, Heena, Samant, Abhay, Guizani, Mohsen.  2019.  A Bio-Inspired Framework to Mitigate DoS Attacks in Software Defined Networking. 2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS). :1–5.
Software Defined Networking (SDN) is an emerging architecture providing services on a priority basis for real-time communication, by pulling out the intelligence from the hardware and developing a better management system for effective networking. Denial of service (DoS) attacks pose a significant threat to SDN, as it can disable the genuine hosts and routers by exhausting their resources. It is thus vital to provide efficient traffic management, both at the data layer and the control layer, thereby becoming more responsive to dynamic network threats such as DoS. Existing DoS prevention and mitigation models for SDN are computationally expensive and are slow to react. This paper introduces a novel biologically inspired architecture for SDN to detect DoS flooding attacks. The proposed biologically inspired architecture utilizes the concepts of the human immune system to provide a robust solution against DoS attacks in SDNs. The two layer immune inspired framework, viz innate layer and adaptive layer, is initiated at the data layer and the control layer of SDN, respectively. The proposed model is reactive and lightweight for DoS mitigation in SDNs.
Kern, Alexander, Anderl, Reiner.  2019.  Securing Industrial Remote Maintenance Sessions using Software-Defined Networking. 2019 Sixth International Conference on Software Defined Systems (SDS). :72–79.
Many modern business models of the manufacturing industry use the possibilities of digitization. In particular, the idea of connecting machines to networks and communication infrastructure is gaining momentum. However, in addition to the considerable economic advantages, this development also brings decisive disadvantages. By connecting previously encapsulated industrial networks with untrustworthy external networks such as the Internet, machines and systems are suddenly exposed to the same threats as conventional IT systems. A key problem today is the typical network paradigm with static routers and switches that cannot meet the dynamic requirements of a modern industrial network. Current security solutions often only threat symptoms instead of tackling the cause. In this paper we will therefore analyze the weaknesses of current networks and security solutions using the example of industrial remote maintenance. We will then present a novel concept of how Software-Defined Networking (SDN) in combination with a policy framework that supports attribute-based access control can be used to meet current and future security requirements in dynamic industrial networks. Furthermore, we will introduce an examplary implementation of this novel security framework for the use case of industrial remote maintenance and evaluate the solution. Our results show that SDN in combination with an Attribute-based Access Control (ABAC) policy framework is perfectly suited to increase flexibility and security of modern industrial networks at the same time.
Tejendra, D.S., Varunkumar, C.R., Sriram, S.L., Sumathy, V., Thejeshwari, C.K..  2019.  A Novel Approach to reduce Vulnerability on Router by Zero vulnerability Encrypted password in Router (ZERO) Mechanism. 2019 3rd International Conference on Computing and Communications Technologies (ICCCT). :163–167.
As technology is developing exponentially and the world is moving towards automation, the resources have to be transferred through the internet which requires routers to connect networks and forward bundles (information). Due to the vulnerability of routers the data and resources have been hacked. The vulnerability of routers is due to minimum authentication to the network shared, some technical attacks on routers, leaking of passwords to others, single passwords. Based on the study, the solution is to maximize authentication of the router by embedding an application that monitors the user entry based on MAC address of the device, the password is frequently changed and that encrypted password is sent to a user and notifies the admin about the changes. Thus, these routers provide high-level security to the forward data through the internet.
Daoud, Luka, Rafla, Nader.  2019.  Analysis of Black Hole Router Attack in Network-on-Chip. 2019 IEEE 62nd International Midwest Symposium on Circuits and Systems (MWSCAS). :69–72.
Network-on-Chip (NoC) is the communication platform of the data among the processing cores in Multiprocessors System-on-Chip (MPSoC). NoC has become a target to security attacks and by outsourcing design, it can be infected with a malicious Hardware Trojan (HT) to degrades the system performance or leaves a back door for sensitive information leaking. In this paper, we proposed a HT model that applies a denial of service attack by deliberately discarding the data packets that are passing through the infected node creating a black hole in the NoC. It is known as Black Hole Router (BHR) attack. We studied the effect of the BHR attack on the NoC. The power and area overhead of the BHR are analyzed. We studied the effect of the locations of BHRs and their distribution in the network as well. The malicious nodes has very small area and power overhead, 1.98% and 0.74% respectively, with a very strong violent attack.
Xuewei, Feng, Dongxia, Wang, Zhechao, Lin.  2019.  An Approach of Code Pointer Hiding Based on a Resilient Area. 2019 Seventh International Conference on Advanced Cloud and Big Data (CBD). :204–209.
Code reuse attacks can bypass the DEP mechanism effectively. Meanwhile, because of the stealthy of the operation, it becomes one of the most intractable threats while securing the information system. Although the security solutions of code randomization and diversity can mitigate the threat at a certain extent, attackers can bypass these solutions due to the high cost and coarsely granularity, and the memory disclosure vulnerability is another magic weapon which can be used by attackers to bypass these solutions. After analyzing the principle of memory disclosure vulnerability, we propose a novel code pointer hiding method based on a resilient area. We expatiate how to create the resilient area and achieve code pointer hiding from four aspects, namely hiding return addresses in data pages, hiding function pointers in data pages, hiding target pointers of instruction JUMP in code pages, and hiding target pointers of instruction CALL in code pages. This method can stop attackers from reading and analyzing pages in memory, which is a critical stage in finding and creating ROP chains while executing a code reuse attack. Lastly, we test the method contrastively, and the results show that the method is feasible and effective while defending against ROP attacks.
Kaul, Sonam Devgan, Hatzinakos, Dimitrios.  2019.  Learning Automata Based Secure Multi Agent RFID Authentication System. 2019 10th International Conference on Computing, Communication and Networking Technologies (ICCCNT). :1–7.
Radio frequency identification wireless sensing technology widely adopted and developed from last decade and has been utilized for monitoring and autonomous identification of objects. However, wider utilization of RFID technologies has introduced challenges such as preserving security and privacy of sensitive data while maintaining the high quality of service. Thus, in this work, we will deliberately build up a RFID system by utilizing learning automata based multi agent intelligent system to greatly enhance and secure message transactions and to improve operational efficiency. The incorporation of these two advancements and technological developments will provide maximum benefit in terms of expertly and securely handle data in RFID scenario. In proposed work, learning automata inbuilt RFID tags or assumed players choose their optimal strategy via enlarging its own utility function to achieve long term benefit. This is possible if they transmit their utility securely to back end server and then correspondingly safely get new utility function from server to behave optimally in its environment. Hence, our proposed authentication protocol, expertly transfer utility from learning automata inbuilt tags to reader and then to server. Moreover, we verify the security and privacy of our proposed system by utilizing automatic formal prover Scyther tool.
Essam, Gehad, Shehata, Heba, Khattab, Tamer, Abualsaud, Khalid, Guizani, Mohsen.  2019.  Novel Hybrid Physical Layer Security Technique in RFID Systems. 2019 15th International Wireless Communications Mobile Computing Conference (IWCMC). :1299–1304.
In this paper, we propose a novel PHY layer security technique in radio frequency identification (RFID) backscatter communications system. In order to protect the RFID tag information confidentiality from the eavesdroppers attacks, the proposed technique deploys beam steering (BS) using a one dimensional (1-D) antenna array in the tag side in addition to noise injection from the reader side. The performance analysis and simulation results show that the new technique outperforms the already-existing noise injection security technique and overcomes its design limitations.
Bothe, Alexander, Bauer, Jan, Aschenbruck, Nils.  2019.  RFID-assisted Continuous User Authentication for IoT-based Smart Farming. 2019 IEEE International Conference on RFID Technology and Applications (RFID-TA). :505–510.
Smart Farming is driven by the emergence of precise positioning systems and Internet of Things technologies which have already enabled site-specific applications, sustainable resource management, and interconnected machinery. Nowadays, so-called Farm Management Information Systems (FMISs) enable farm-internal interconnection of agricultural machines and implements and, thereby, allow in-field data exchange and the orchestration of collaborative agricultural processes. Machine data is often directly logged during task execution. Moreover, interconnection of farms, agricultural contractors, and marketplaces ease the collaboration. However, current FMISs lack in security and particularly in user authentication. In this paper, we present a security architecture for a decentralized, manufacturer-independent, and open-source FMIS. Special attention is turned on the Radio Frequency Identification (RFID)-based continuous user authentication which greatly improves security and credibility of automated documentation, while at the same time preserves usability in practice.
Xu, Yilin, Ge, Weimin, Li, Xiaohong, Feng, Zhiyong, Xie, Xiaofei, Bai, Yude.  2019.  A Co-Occurrence Recommendation Model of Software Security Requirement. 2019 International Symposium on Theoretical Aspects of Software Engineering (TASE). :41–48.
To guarantee the quality of software, specifying security requirements (SRs) is essential for developing systems, especially for security-critical software systems. However, using security threat to determine detailed SR is quite difficult according to Common Criteria (CC), which is too confusing and technical for non-security specialists. In this paper, we propose a Co-occurrence Recommend Model (CoRM) to automatically recommend software SRs. In this model, the security threats of product are extracted from security target documents of software, in which the related security requirements are tagged. In order to establish relationships between software security threat and security requirement, semantic similarities between different security threat is calculated by Skip-thoughts Model. To evaluate our CoRM model, over 1000 security target documents of 9 types software products are exploited. The results suggest that building a CoRM model via semantic similarity is feasible and reliable.
Karlsson, Linus, Paladi, Nicolae.  2019.  Privacy-Enabled Recommendations for Software Vulnerabilities. 2019 IEEE Intl Conf on Dependable, Autonomic and Secure Computing, Intl Conf on Pervasive Intelligence and Computing, Intl Conf on Cloud and Big Data Computing, Intl Conf on Cyber Science and Technology Congress (DASC/PiCom/CBDCom/CyberSciTech). :564–571.
New software vulnerabilities are published daily. Prioritizing vulnerabilities according to their relevance to the collection of software an organization uses is a costly and slow process. While recommender systems were earlier proposed to address this issue, they ignore the security of the vulnerability prioritization data. As a result, a malicious operator or a third party adversary can collect vulnerability prioritization data to identify the security assets in the enterprise deployments of client organizations. To address this, we propose a solution that leverages isolated execution to protect the privacy of vulnerability profiles without compromising data integrity. To validate an implementation of the proposed solution we integrated it with an existing recommender system for software vulnerabilities. The evaluation of our implementation shows that the proposed solution can effectively complement existing recommender systems for software vulnerabilities.
Bibi, Iram, Akhunzada, Adnan, Malik, Jahanzaib, Ahmed, Ghufran, Raza, Mohsin.  2019.  An Effective Android Ransomware Detection Through Multi-Factor Feature Filtration and Recurrent Neural Network. 2019 UK/ China Emerging Technologies (UCET). :1–4.
With the increasing diversity of Android malware, the effectiveness of conventional defense mechanisms are at risk. This situation has endorsed a notable interest in the improvement of the exactitude and scalability of malware detection for smart devices. In this study, we have proposed an effective deep learning-based malware detection model for competent and improved ransomware detection in Android environment by looking at the algorithm of Long Short-Term Memory (LSTM). The feature selection has been done using 8 different feature selection algorithms. The 19 important features are selected through simple majority voting process by comparing results of all feature filtration techniques. The proposed algorithm is evaluated using android malware dataset (CI-CAndMal2017) and standard performance parameters. The proposed model outperforms with 97.08% detection accuracy. Based on outstanding performance, we endorse our proposed algorithm to be efficient in malware and forensic analysis.
2020-03-18
Uthayashangar, S., Dhamini, P., Mahalakshmi, M., Mangayarkarasi, V..  2019.  Efficient Group Data Sharing In Cloud Environment Using Honey Encryption. 2019 IEEE International Conference on System, Computation, Automation and Networking (ICSCAN). :1–3.
Cloud computing is a rapid growing advanced technology which is Internet based, providing various ways for storage, resource sharing, and various features. It has brought a new way to securely store and share information and data with multiple users and groups. The cloud environment deals with many problems, and one of the most important problems in recent days is the security issues. Sharing the data in a group, in cloud conditions has turned into a blazing theme in up and coming decades. Thus the blasting interest in cloud computing, ways and measures to accomplish secure and effective information and data sharing in the cloud is a flourishing point to be engaged. In this way, the venture centers around empowering information sharing and capacity for a similar gathering inside the cloud with high security and intensity. Therefore, Honey Encryption and Advanced Encryption Standard is used for providing security for the data shared within the group by the crew members in cloud environment. In addition, an access key is provided by the Group Manager to enable access to the documents and files stored in cloud by the users for specific time period.
Shah, Meet D., Mohanty, Manoranjan, Atrey, Pradeep K..  2019.  SecureCSearch: Secure Searching in PDF Over Untrusted Cloud Servers. 2019 IEEE Conference on Multimedia Information Processing and Retrieval (MIPR). :347–352.
The usage of cloud for data storage has become ubiquitous. To prevent data leakage and hacks, it is common to encrypt the data (e.g. PDF files) before sending it to a cloud. However, this limits the search for specific files containing certain keywords over an encrypted cloud data. The traditional method is to take down all files from a cloud, store them locally, decrypt and then search over them, defeating the purpose of using a cloud. In this paper, we propose a method, called SecureCSearch, to perform keyword search operations on the encrypted PDF files over cloud in an efficient manner. The proposed method makes use of Shamir's Secret Sharing scheme in a novel way to create encrypted shares of the PDF file and the keyword to search. We show that the proposed method maintains the security of the data and incurs minimal computation cost.
jaidane, Emna, Hamdi, Mohamed, Aguili, Taoufik, Kim, Tai-hoon.  2019.  A new vehicular blackbox architecture based on searchable encryption. 2019 15th International Wireless Communications Mobile Computing Conference (IWCMC). :1073–1078.
Blackboxes are being increasingly used in the vehicular context to store and transmit information related to safety, security and many other applications. The plethora of sensors available at the different parts of the vehicle can provide enriched gathering of the data related to these applications. Nonetheless, to support multiple use cases, the blackbox must be accessible by various actors (e.g. vehicle owner, insurance company, law enforcement authorities). This raises significant challenges regarding the privacy of the data collected and stored in the blackbox. In fact, these data can often lead to tracing back accurate facts about the behaviour of the owner of the vehicle. To cope with this problem, we propose a new blackbox architecture supporting searchable encryption. This feature allows multiple users who are not able to decipher the content of the blackbox to validate properties such as path traceback and velocity. To illustrate the implementation of the proposed technique in practice, we discuss a case study related to post-accident processing by insurance companies.
Mei, Lei, Tong, Haojie, Liu, Tong, Tian, Ye.  2019.  PSA: An Architecture for Proactively Securing Protocol-Oblivious SDN Networks. 2019 IEEE 9th International Conference on Electronics Information and Emergency Communication (ICEIEC). :1–6.

Up to now, Software-defined network (SDN) has been developing for many years and various controller implementations have appeared. Most of these controllers contain the normal business logic as well as security defense function. This makes the business logic on the controller tightly coupled with the security function, which increases the burden of the controller and is not conducive to the evolution of the controller. To address this problem, we propose a proactive security framework PSA, which decouples the business logic and security function of the controller, and deploys the security function in the proactive security layer which lies between the data plane and the control plane, so as to provide a unified security defense framework for different controller implementations. Based on PSA, we design a security defense application for the data-to-control plane saturation attack, which overloads the infrastructure of SDN networks. We evaluate the prototype implementation of PSA in the software environments. The results show that PSA is effective with adding only minor overhead into the entire SDN infrastructure.

Zkik, Karim, Sebbar, Anass, Baadi, Youssef, Belhadi, Amine, Boulmalf, Mohammed.  2019.  An efficient modular security plane AM-SecP for hybrid distributed SDN. 2019 International Conference on Wireless and Mobile Computing, Networking and Communications (WiMob). :354–359.

Software defined networks (SDNs) represent new centralized network architecture that facilitates the deployment of services, applications and policies from the upper layers, relatively the management and control planes to the lower layers the data plane and the end user layer. SDNs give several advantages in terms of agility and flexibility, especially for mobile operators and for internet service providers. However, the implementation of these types of networks faces several technical challenges and security issues. In this paper we will focus on SDN's security issues and we will propose the implementation of a centralized security layer named AM-SecP. The proposed layer is linked vertically to all SDN layers which ease packets inspections and detecting intrusions. The purpose of this architecture is to stop and to detect malware infections, we do this by denying services and tunneling attacks without encumbering the networks by expensive operations and high calculation cost. The implementation of the proposed framework will be also made to demonstrate his feasibility and robustness.

Williams, Laurie.  2019.  Science Leaves Clues. IEEE Security Privacy. 17:4–6.
The elusive science of security. Science advances when research results build upon prior findings through the evolution of hypotheses and theories about the fundamental relationships among variables within a context and considering the threats and limitations of the work. Some hypothesize that, through this science of security, the industry can take a more principled and systematic approach to securing systems, rather than reacting to the latest move by attackers. Others debate the utility of a science of security.
2020-03-16
Zebari, Dilovan Asaad, Haron, Habibollah, Zeebaree, Diyar Qader, Zain, Azlan Mohd.  2019.  A Simultaneous Approach for Compression and Encryption Techniques Using Deoxyribonucleic Acid. 2019 13th International Conference on Software, Knowledge, Information Management and Applications (SKIMA). :1–6.
The Data Compression is a creative skill which defined scientific concepts of providing contents in a compact form. Thus, it has turned into a need in the field of communication as well as in different scientific studies. Data transmission must be sufficiently secure to be utilized in a channel medium with no misfortune; and altering of information. Encryption is the way toward scrambling an information with the goal that just the known receiver can peruse or see it. Encryption can give methods for anchoring data. Along these lines, the two strategies are the two crucial advances that required for the protected transmission of huge measure of information. In typical cases, the compacted information is encoded and transmitted. In any case, this sequential technique is time consumption and computationally cost. In the present paper, an examination on simultaneous compression and encryption technique depends on DNA which is proposed for various sorts of secret data. In simultaneous technique, both techniques can be done at single step which lessens the time for the whole task. The present work is consisting of two phases. First phase, encodes the plaintext by 6-bits instead of 8-bits, means each character represented by three DNA nucleotides whereas to encode any pixel of image by four DNA nucleotides. This phase can compress the plaintext by 25% of the original text. Second phase, compression and encryption has been done at the same time. Both types of data have been compressed by their half size as well as encrypted the generated symmetric key. Thus, this technique is more secure against intruders. Experimental results show a better performance of the proposed scheme compared with standard compression techniques.
White, Ruffin, Caiazza, Gianluca, Jiang, Chenxu, Ou, Xinyue, Yang, Zhiyue, Cortesi, Agostino, Christensen, Henrik.  2019.  Network Reconnaissance and Vulnerability Excavation of Secure DDS Systems. 2019 IEEE European Symposium on Security and Privacy Workshops (EuroS PW). :57–66.
Data Distribution Service (DDS) is a realtime peer-to-peer protocol that serves as a scalable middleware between distributed networked systems found in many Industrial IoT domains such as automotive, medical, energy, and defense. Since the initial ratification of the standard, specifications have introduced a Security Model and Service Plugin Interface (SPI) architecture, facilitating authenticated encryption and data centric access control while preserving interoperable data exchange. However, as Secure DDS v1.1, the default plugin specifications presently exchanges digitally signed capability lists of both participants in the clear during the crypto handshake for permission attestation; thus breaching confidentiality of the context of the connection. In this work, we present an attacker model that makes use of network reconnaissance afforded by this leaked context in conjunction with formal verification and model checking to arbitrarily reason about the underlying topology and reachability of information flow, enabling targeted attacks such as selective denial of service, adversarial partitioning of the data bus, or vulnerability excavation of vendor implementations.
Tahat, Amer, Joshi, Sarang, Goswami, Pronnoy, Ravindran, Binoy.  2019.  Scalable Translation Validation of Unverified Legacy OS Code. 2019 Formal Methods in Computer Aided Design (FMCAD). :1–9.
Formally verifying functional and security properties of a large-scale production operating system is highly desirable. However, it is challenging as such OSes are often written in multiple source languages that have no formal semantics - a prerequisite for formal reasoning. To avoid expensive formalization of the semantics of multiple high-level source languages, we present a lightweight and rigorous verification toolchain that verifies OS code at the binary level, targeting ARM machines. To reason about ARM instructions, we first translate the ARM Specification Language that describes the semantics of the ARMv8 ISA into the PVS7 theorem prover and verify the translation. We leverage the radare2 reverse engineering tool to decode ARM binaries into PVS7 and verify the translation. Our translation verification methodology is a lightweight formal validation technique that generates large-scale instruction emulation test lemmas whose proof obligations are automatically discharged. To demonstrate our verification methodology, we apply the technique on two OSes: Google's Zircon and a subset of Linux. We extract a set of 370 functions from these OSes, translate them into PVS7, and verify the correctness of the translation by automatically discharging hundreds of thousands of proof obligations and tests. This took 27.5 person-months to develop.
Sandor, Hunor, Genge, Bela, Haller, Piroska, Bica, Andrei.  2019.  A Security-Enhanced Interoperability Middleware for the Internet of Things. 2019 7th International Symposium on Digital Forensics and Security (ISDFS). :1–6.
This paper documents an Internet of Things (IoT) middleware specially tailored to address the security, and operational requirements expected from an effective IoT platform. In essence, the middleware exposes a diverse palette of features, including authentication, authorization, auditing, confidentiality and integrity of data. Besides these aspects, the middleware encapsulates an IoT object abstraction layer that builds a generic object model that is independent from the device type (i.e., hardware, software, vendor). Furthermore, it builds on standards and specifications to accomplish a highly resilient and scalable solution. The approach is tested on several hardware platforms. A use case scenario is presented to demonstrate its main features. The middleware represents a key component in the context of the “GHOST - Safe-Guarding Home IoT Environments with Personalised Real-time Risk Control” project.