Visible to the public Biblio

Filters: Keyword is sandbox  [Clear All Filters]
2023-02-17
Rekeraho, Alexandre, Balan, Titus, Cotfas, Daniel T., Cotfas, Petru A., Acheampong, Rebecca, Musuroi, Cristian.  2022.  Sandbox Integrated Gateway for the Discovery of Cybersecurity Vulnerabilities. 2022 International Symposium on Electronics and Telecommunications (ISETC). :1–4.
Emails are widely used as a form of communication and sharing files in an organization. However, email is widely used by cybercriminals to spread malware and carrying out cyber-attacks. We implemented an open-source email gateway in conjunction with a security sandbox for securing emails against malicious attachments. The email gateway scans all incoming and outgoing emails and stops emails containing suspicious files. An automated python script would then send the suspected email to the sandboxing element through sandbox API for further analysis, while the script is used also for the prevention of duplicate results. Moreover, the mail server administrator receives notifications from the email gateway about suspicious attachments. If detected attachment is a true positive based on the sandbox analysis result, email is deleted, otherwise, the email is delivered to the recipient. The paper describes in an empirical way the steps followed during the implementation, results, and conclusions of our research.
ISSN: 2475-7861
2022-11-02
Liu, I-Hsien, Hsieh, Cheng-En, Lin, Wei-Min, Li, Chu-Fen, Li, Jung-Shian.  2021.  Malicious Flows Generator Based on Data Balanced Algorithm. 2021 International Conference on Fuzzy Theory and Its Applications (iFUZZY). :1–4.
As Internet technology gradually matures, the network structure becomes more complex. Therefore, the attack methods of malicious attackers are more diverse and change faster. Fortunately, due to the substantial increase in computer computing power, machine learning is valued and widely used in various fields. It has also been applied to intrusion detection systems. This study found that due to the imperfect data ratio of the unbalanced flow dataset, the model will be overfitting and the misjudgment rate will increase. In response to this problem, this research proposes to use the Cuckoo system to induce malicious samples to generate malicious traffic, to solve the data proportion defect of the unbalanced traffic dataset.
2022-03-14
Vykopal, Jan, Čeleda, Pavel, Seda, Pavel, Švábenský, Valdemar, Tovarňák, Daniel.  2021.  Scalable Learning Environments for Teaching Cybersecurity Hands-on. 2021 IEEE Frontiers in Education Conference (FIE). :1—9.
This Innovative Practice full paper describes a technical innovation for scalable teaching of cybersecurity hands-on classes using interactive learning environments. Hands-on experience significantly improves the practical skills of learners. However, the preparation and delivery of hands-on classes usually do not scale. Teaching even small groups of students requires a substantial effort to prepare the class environment and practical assignments. Further issues are associated with teaching large classes, providing feedback, and analyzing learning gains. We present our research effort and practical experience in designing and using learning environments that scale up hands-on cybersecurity classes. The environments support virtual networks with full-fledged operating systems and devices that emulate realworld systems. The classes are organized as simultaneous training sessions with cybersecurity assignments and learners' assessment. For big classes, with the goal of developing learners' skills and providing formative assessment, we run the environment locally, either in a computer lab or at learners' own desktops or laptops. For classes that exercise the developed skills and feature summative assessment, we use an on-premises cloud environment. Our approach is unique in supporting both types of deployment. The environment is described as code using open and standard formats, defining individual hosts and their networking, configuration of the hosts, and tasks that the students have to solve. The environment can be repeatedly created for different classes on a massive scale or for each student on-demand. Moreover, the approach enables learning analytics and educational data mining of learners' interactions with the environment. These analyses inform the instructor about the student's progress during the class and enable the learner to reflect on a finished training. Thanks to this, we can improve the student class experience and motivation for further learning. Using the presented environments KYPO Cyber Range Platform and Cyber Sandbox Creator, we delivered the classes on-site or remotely for various target groups of learners (K-12, university students, and professional learners). The learners value the realistic nature of the environments that enable exercising theoretical concepts and tools. The instructors value time-efficiency when preparing and deploying the hands-on activities. Engineering and computing educators can freely use our software, which we have released under an open-source license. We also provide detailed documentation and exemplary hands-on training to help other educators adopt our teaching innovations and enable sharing of reusable components within the community.
Correa, Mauricio, GOMEZ, Tomás, Cossent, Rafael.  2021.  Local Flexibility Mechanisms for Electricity Distribution Through Regulatory Sandboxes: International Review and a Proposal for Spain. 2021 IEEE Madrid PowerTech. :1—6.
The EU goal of achieving carbon neutrality by 2050 will require profound changes in the electricity supply chain. In this context, Distribution System Operators (DSOs) are expected to adopt solutions to efficiently integrate distributed energy resources (DER), including the implementation of local flexibility mechanisms. Thus, DSOs would procure services from DER like distributed generation, demand response, or storage to support grid expansion, attain significant cost savings, and swifter DER integration. However, the use of flexibility mechanisms still faces barriers posed by national regulation. Regulatory sandboxes may be used to overcome this gap by enabling and supporting the development of local flexibility mechanisms. This paper performs an international review of four leading countries in the use of sandbox and flexibility, identifies best practices, and, based on the lessons learned, provides recommendations to implement local flexibility mechanisms for DSOs in Spain under regulatory sandboxes
2022-01-10
Jianhua, Xing, Jing, Si, Yongjing, Zhang, Wei, Li, Yuning, Zheng.  2021.  Research on Malware Variant Detection Method Based on Deep Neural Network. 2021 IEEE 5th International Conference on Cryptography, Security and Privacy (CSP). :144–147.
To deal with the increasingly serious threat of industrial information malicious code, the simulations and characteristics of the domestic security and controllable operating system and office software were implemented in the virtual sandbox environment based on virtualization technology in this study. Firstly, the serialization detection scheme based on the convolution neural network algorithm was improved. Then, the API sequence was modeled and analyzed by the improved convolution neural network algorithm to excavate more local related information of variant sequences. Finally the variant detection of malicious code was realized. Results showed that this improved method had higher efficiency and accuracy for a large number of malicious code detection, and could be applied to the malicious code detection in security and controllable operating system.
2021-09-21
Vurdelja, Igor, Blažić, Ivan, Bojić, Dragan, Drašković, Dražen.  2020.  A framework for automated dynamic malware analysis for Linux. 2020 28th Telecommunications Forum (℡FOR). :1–4.
Development of malware protection tools requires a more advanced test environment comparing to safe software. This kind of development includes a safe execution of many malware samples in order to evaluate the protective power of the tool. The host machine needs to be protected from the harmful effects of malware samples and provide a realistic simulation of the execution environment. In this paper, a framework for automated malware analysis on Linux is presented. Different types of malware analysis methods are discussed, as well as the properties of a good framework for dynamic malware analysis.
2021-05-05
Chi, Po-Wen, Wang, Ming-Hung, Zheng, Yu.  2020.  SandboxNet: An Online Malicious SDN Application Detection Framework for SDN Networking. 2020 International Computer Symposium (ICS). :397—402.

Software Defined Networking (SDN) is a concept that decouples the control plane and the user plane. So the network administrator can easily control the network behavior through its own programs. However, the administrator may unconsciously apply some malicious programs on SDN controllers so that the whole network may be under the attacker’s control. In this paper, we discuss the malicious software issue on SDN networks. We use the idea of sandbox to propose a sandbox network called SanboxNet. We emulate a virtual isolated network environment to verify the SDN application functions. With continuous monitoring, we can locate the suspicious SDN applications. We also consider the sandbox-evading issue in our framework. The emulated networks and the real world networks will be indistinguishable to the SDN controller.

Kishore, Pushkar, Barisal, Swadhin Kumar, Prasad Mohapatra, Durga.  2020.  JavaScript malware behaviour analysis and detection using sandbox assisted ensemble model. 2020 IEEE REGION 10 CONFERENCE (TENCON). :864—869.

Whenever any internet user visits a website, a scripting language runs in the background known as JavaScript. The embedding of malicious activities within the script poses a great threat to the cyberworld. Attackers take advantage of the dynamic nature of the JavaScript and embed malicious code within the website to download malware and damage the host. JavaScript developers obfuscate the script to keep it shielded from getting detected by the malware detectors. In this paper, we propose a novel technique for analysing and detecting JavaScript using sandbox assisted ensemble model. We extract the payload using malware-jail sandbox to get the real script. Upon getting the extracted script, we analyse it to define the features that are needed for creating the dataset. We compute Pearson's r between every feature for feature extraction. An ensemble model consisting of Sequential Minimal Optimization (SMO), Voted Perceptron and AdaBoost algorithm is used with voting technique to detect malicious JavaScript. Experimental results show that our proposed model can detect obfuscated and de-obfuscated malicious JavaScript with an accuracy of 99.6% and 0.03s detection time. Our model performs better than other state-of-the-art models in terms of accuracy and least training and detection time.

Đuranec, A., Gruičić, S., Žagar, M..  2020.  Forensic analysis of Windows 10 Sandbox. 2020 43rd International Convention on Information, Communication and Electronic Technology (MIPRO). :1224—1229.

With each Windows operating system Microsoft introduces new features to its users. Newly added features present a challenge to digital forensics examiners as they are not analyzed or tested enough. One of the latest features, introduced in Windows 10 version 1909 is Windows Sandbox; a lightweight, temporary, environment for running untrusted applications. Because of the temporary nature of the Sandbox and insufficient documentation, digital forensic examiners are facing new challenges when examining this newly added feature which can be used to hide different illegal activities. Throughout this paper, the focus will be on analyzing different Windows artifacts and event logs, with various tools, left behind as a result of the user interaction with the Sandbox feature on a clear virtual environment. Additionally, the setup of testing environment will be explained, the results of testing and interpretation of the findings will be presented, as well as open-source tools used for the analysis.

Rizvi, Syed R, Lubawy, Andrew, Rattz, John, Cherry, Andrew, Killough, Brian, Gowda, Sanjay.  2020.  A Novel Architecture of Jupyterhub on Amazon Elastic Kubernetes Service for Open Data Cube Sandbox. IGARSS 2020 - 2020 IEEE International Geoscience and Remote Sensing Symposium. :3387—3390.

The Open Data Cube (ODC) initiative, with support from the Committee on Earth Observation Satellites (CEOS) System Engineering Office (SEO) has developed a state-of-the-art suite of software tools and products to facilitate the analysis of Earth Observation data. This paper presents a short summary of our novel architecture approach in a project related to the Open Data Cube (ODC) community that provides users with their own ODC sandbox environment. Users can have a sandbox environment all to themselves for the purpose of running Jupyter notebooks that leverage the ODC. This novel architecture layout will remove the necessity of hosting multiple users on a single Jupyter notebook server and provides better management tooling for handling resource usage. In this new layout each user will have their own credentials which will give them access to a personal Jupyter notebook server with access to a fully deployed ODC environment enabling exploration of solutions to problems that can be supported by Earth observation data.

2020-03-27
Al-Rushdan, Huthifh, Shurman, Mohammad, Alnabelsi, Sharhabeel H., Althebyan, Qutaibah.  2019.  Zero-Day Attack Detection and Prevention in Software-Defined Networks. 2019 International Arab Conference on Information Technology (ACIT). :278–282.

The zero-day attack in networks exploits an undiscovered vulnerability, in order to affect/damage networks or programs. The term “zero-day” refers to the number of days available to the software or the hardware vendor to issue a patch for this new vulnerability. Currently, the best-known defense mechanism against the zero-day attacks focuses on detection and response, as a prevention effort, which typically fails against unknown or new vulnerabilities. To the best of our knowledge, this attack has not been widely investigated for Software-Defined Networks (SDNs). Therefore, in this work we are motivated to develop anew zero-day attack detection and prevention mechanism, which is designed and implemented for SDN using a modified sandbox tool, named Cuckoo. Our experiments results, under UNIX system, show that our proposed design successfully stops zero-day malwares by isolating the infected client, and thus, prevents these malwares from infesting other clients.

Walker, Aaron, Amjad, Muhammad Faisal, Sengupta, Shamik.  2019.  Cuckoo’s Malware Threat Scoring and Classification: Friend or Foe? 2019 IEEE 9th Annual Computing and Communication Workshop and Conference (CCWC). :0678–0684.
Malware threat classification involves understanding the behavior of the malicious software and how it affects a victim host system. Classifying threats allows for measured response appropriate to the risk involved. Malware incident response depends on many automated tools for the classification of threat to help identify the appropriate reaction to a threat alert. Cuckoo Sandbox is one such tool which can be used for automated analysis of malware and one method of threat classification provided is a threat score. A security analyst might submit a suspicious file to Cuckoo for analysis to determine whether or not the file contains malware or performs potentially malicious behavior on a system. Cuckoo is capable of producing a report of this behavior and ranks the severity of the observed actions as a score from one to ten, with ten being the most severe. As such, a malware sample classified as an 8 would likely take priority over a sample classified as a 3. Unfortunately, this scoring classification can be misleading due to the underlying methodology of severity classification. In this paper we demonstrate why the current methodology of threat scoring is flawed and therefore we believe it can be improved with greater emphasis on analyzing the behavior of the malware. This allows for a threat classification rating which scales with the risk involved in the malware behavior.
2019-09-26
Reijers, Niels, Shih, Chi-Sheng.  2018.  CapeVM: A Safe and Fast Virtual Machine for Resource-Constrained Internet-of-Things Devices. Proceedings of the 16th ACM Conference on Embedded Networked Sensor Systems. :250-263.

This paper presents CapeVM, a sensor node virtual machine aimed at delivering both high performance and a sandboxed execution environment that ensures malicious code cannot corrupt the VM's internal state or perform actions not allowed by the VM. CapeVM uses Ahead-of-Time compilation and introduces a range of optimisations to eliminate most of the overhead present in previous work on sensor node AOT compilers. A sandboxed execution environment is guaranteed by a set of checks. The structured nature of the VM's instruction set allows the VM to perform most checks at load time, reducing the need for expensive run-time checks compared to native code approaches. While some overhead from using a VM and adding sandbox checks cannot be avoided, CapeVM's optimisations reduce this overhead dramatically. We evaluate CapeVM using a set of IoT applications and show this results in a performance just 2.1x slower than unsandboxed native code. Thus, CapeVM combines the desirable properties ofexisting work on both sandboxed execution and virtual machines for sensor nodes, with significantly improved performance.

2019-06-24
Wright, D., Stroschein, J..  2018.  A Malware Analysis and Artifact Capture Tool. 2018 IEEE 16th Intl Conf on Dependable, Autonomic and Secure Computing, 16th Intl Conf on Pervasive Intelligence and Computing, 4th Intl Conf on Big Data Intelligence and Computing and Cyber Science and Technology Congress(DASC/PiCom/DataCom/CyberSciTech). :328–333.

Malware authors attempt to obfuscate and hide their code in its static and dynamic states. This paper provides a novel approach to aid analysis by intercepting and capturing malware artifacts and providing dynamic control of process flow. Capturing malware artifacts allows an analyst to more quickly and comprehensively understand malware behavior and obfuscation techniques and doing so interactively allows multiple code paths to be explored. The faster that malware can be analyzed the quicker the systems and data compromised by it can be determined and its infection stopped. This research proposes an instantiation of an interactive malware analysis and artifact capture tool.

2018-05-09
Chang, Kai-Chi, Tso, Raylin, Tsai, Min-Chun.  2017.  IoT Sandbox: To Analysis IoT Malware Zollard. Proceedings of the Second International Conference on Internet of Things and Cloud Computing. :4:1–4:8.

As we know, we are already facing IoT threat and under IoT attacks. However, there are only a few discussions on, how to analyze this kind of cyber threat and malwares. In this paper, we propose IoT sandbox which can support different type of CPU architecture. It can be used to analyze IoT malwares, collect network packets, identify spread method and record malwares behaviors. To make sure our IoT sandbox can be functional, we implement it and use the Zollard botnet for experiment. According to our experimental data, we found that at least 71,148 IP have been compromised. Some of them are IoT devices (DVR, Web Camera, Router WiFi Disk, Set-top box) and others are ICS devices (Heat pump and ICS data acquisition server). Based on our IoT sandbox technology, we can discover an IoT malware in an early stage. This could help IT manager or security experts to analysis and determine IDS rules. We hope this research can prevent IoT threat and enhance IoT Security in the near future.

Witt, M., Jansen, C., Krefting, D., Streit, A..  2017.  Fine-Grained Supervision and Restriction of Biomedical Applications in Linux Containers. 2017 17th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing (CCGRID). :813–822.

Applications for data analysis of biomedical data are complex programs and often consist of multiple components. Re-usage of existing solutions from external code repositories or program libraries is common in algorithm development. To ease reproducibility as well as transfer of algorithms and required components into distributed infrastructures Linux containers are increasingly used in those environments, that are at least partly connected to the internet. However concerns about the untrusted application remain and are of high interest when medical data is processed. Additionally, the portability of the containers needs to be ensured by using only security technologies, that do not require additional kernel modules. In this paper we describe measures and a solution to secure the execution of an example biomedical application for normalization of multidimensional biosignal recordings. This application, the required runtime environment and the security mechanisms are installed in a Docker-based container. A fine-grained restricted environment (sandbox) for the execution of the application and the prevention of unwanted behaviour is created inside the container. The sandbox is based on the filtering of system calls, as they are required to interact with the operating system to access potentially restricted resources e.g. the filesystem or network. Due to the low-level character of system calls, the creation of an adequate rule set for the sandbox is challenging. Therefore the presented solution includes a monitoring component to collect required data for defining the rules for the application sandbox. Performance evaluation of the application execution shows no significant impact of the resulting sandbox, while detailed monitoring may increase runtime up to over 420%.

2018-04-04
Ficco, M., Venticinque, S., Rak, M..  2017.  Malware Detection for Secure Microgrids: CoSSMic Case Study. 2017 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData). :336–341.

Information and communication technologies are extensively used to monitor and control electric microgrids. Although, such innovation enhance self healing, resilience, and efficiency of the energy infrastructure, it brings emerging security threats to be a critical challenge. In the context of microgrid, the cyber vulnerabilities may be exploited by malicious users for manipulate system parameters, meter measurements and price information. In particular, malware may be used to acquire direct access to monitor and control devices in order to destabilize the microgrid ecosystem. In this paper, we exploit a sandbox to analyze security vulnerability to malware of involved embedded smart-devices, by monitoring at different abstraction levels potential malicious behaviors. In this direction, the CoSSMic project represents a relevant case study.

2018-01-16
Miramirkhani, N., Appini, M. P., Nikiforakis, N., Polychronakis, M..  2017.  Spotless Sandboxes: Evading Malware Analysis Systems Using Wear-and-Tear Artifacts. 2017 IEEE Symposium on Security and Privacy (SP). :1009–1024.

Malware sandboxes, widely used by antivirus companies, mobile application marketplaces, threat detection appliances, and security researchers, face the challenge of environment-aware malware that alters its behavior once it detects that it is being executed on an analysis environment. Recent efforts attempt to deal with this problem mostly by ensuring that well-known properties of analysis environments are replaced with realistic values, and that any instrumentation artifacts remain hidden. For sandboxes implemented using virtual machines, this can be achieved by scrubbing vendor-specific drivers, processes, BIOS versions, and other VM-revealing indicators, while more sophisticated sandboxes move away from emulation-based and virtualization-based systems towards bare-metal hosts. We observe that as the fidelity and transparency of dynamic malware analysis systems improves, malware authors can resort to other system characteristics that are indicative of artificial environments. We present a novel class of sandbox evasion techniques that exploit the "wear and tear" that inevitably occurs on real systems as a result of normal use. By moving beyond how realistic a system looks like, to how realistic its past use looks like, malware can effectively evade even sandboxes that do not expose any instrumentation indicators, including bare-metal systems. We investigate the feasibility of this evasion strategy by conducting a large-scale study of wear-and-tear artifacts collected from real user devices and publicly available malware analysis services. The results of our evaluation are alarming: using simple decision trees derived from the analyzed data, malware can determine that a system is an artificial environment and not a real user device with an accuracy of 92.86%. As a step towards defending against wear-and-tear malware evasion, we develop statistical models that capture a system's age and degree of use, which can be used to aid sandbox operators in creating system i- ages that exhibit a realistic wear-and-tear state.

2017-12-20
Narvekar, A. N., Joshi, K. K..  2017.  Security sandbox model for modern web environment. 2017 International Conference on Nascent Technologies in Engineering (ICNTE). :1–6.
We require a very good technical knowledge to create automated tests to exploit the browser vulnerabilities. It is usually a combination of technical abilities and set of specific tools. Security concerns is of prime importance when it comes to web browsers. Attacks during surfing, executing any downloaded file and while transmission are very frequent these days and hence all browsers need to be hardened to ensure security. Sandbox is one of the feature where we can prevent malicious applications to run directly on hardware. It is an environment where new or non-trusted applications are executed. Many leading web browsers are trying their level best to implement sandbox. In this paper, we have mentioned the basic necessity of sandbox, current implementations in different web browsers and also present a self-proposed approach.
2017-11-20
Haq, M. S. Ul, Lejian, L., Lerong, M..  2016.  Transitioning Native Application into Virtual Machine by Using Hardware Virtualization Extensions. 2016 International Symposium on Computer, Consumer and Control (IS3C). :397–403.

In presence of known and unknown vulnerabilities in code and flow control of programs, virtual machine alike isolation and sandboxing to confine maliciousness of process, by monitoring and controlling the behaviour of untrusted application, is an effective strategy. A confined malicious application cannot effect system resources and other applications running on same operating system. But present techniques used for sandboxing have some drawbacks ranging from scope to methodology. Some of proposed techniques restrict specific aspect of execution e.g. system calls and file system access. In the same way techniques that truly isolate the application by providing separate execution environment either require modification in kernel or full blown operating system. Moreover these do not provide isolation from top to bottom but only virtualize operating system services. In this paper, we propose a design to confine native Linux process in virtual machine equivalent isolation by using hardware virtualization extensions with nominal initialization and acceptable execution overheads. We implemented our prototype called Process Virtual Machine that transition a native process into virtual machine, provides minimal possible execution environment, intercept and virtualize system calls to execute it on host kernel. Experimental results show effectiveness of our proposed technique.

2017-11-13
Chang, Rui, Jiang, Liehui, Yin, Qing, Ren, Lu, Liu, Qingfeng.  2016.  An Effective Usage and Access Control Scheme for Preventing Permission Leak in a Trusted Execution Environment. Proceedings of the 6th International Conference on Communication and Network Security. :6–10.

In the universal Android system, each application runs in its own sandbox, and the permission mechanism is used to enforce access control to the system APIs and applications. However, permission leak could happen when an application without certain permission illegally gain access to protected resources through other privileged applications. In order to address permission leak in a trusted execution environment, this paper designs security architecture which contains sandbox module, middleware module, usage and access control module, and proposes an effective usage and access control scheme that can prevent permission leak in a trusted execution environment. Security architecture based on the scheme has been implemented on an ARM-Android platform, and the evaluation of the proposed scheme demonstrates its effectiveness in mitigating permission leak vulnerabilities.

2017-03-20
Deshotels, Luke, Deaconescu, Razvan, Chiroiu, Mihai, Davi, Lucas, Enck, William, Sadeghi, Ahmad-Reza.  2016.  SandScout: Automatic Detection of Flaws in iOS Sandbox Profiles. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :704–716.

Recent literature on iOS security has focused on the malicious potential of third-party applications, demonstrating how developers can bypass application vetting and code-level protections. In addition to these protections, iOS uses a generic sandbox profile called "container" to confine malicious or exploited third-party applications. In this paper, we present the first systematic analysis of the iOS container sandbox profile. We propose the SandScout framework to extract, decompile, formally model, and analyze iOS sandbox profiles as logic-based programs. We use our Prolog-based queries to evaluate file-based security properties of the container sandbox profile for iOS 9.0.2 and discover seven classes of exploitable vulnerabilities. These attacks affect non-jailbroken devices running later versions of iOS. We are working with Apple to resolve these attacks, and we expect that SandScout will play a significant role in the development of sandbox profiles for future versions of iOS.

2017-03-08
Guo, Q., Fan, J., Li, N..  2015.  The achieve of power manager application honey-pot based on sandbox. 2015 5th International Conference on Electric Utility Deregulation and Restructuring and Power Technologies (DRPT). :2523–2527.

Honeypot is a common method of attack capture, can maximize the reduction of cyber-attacks. However, its limited application layer simulation makes it impossible to use effectively in power system. Through research on sandboxing technology, this article implements the simulated power manager applications by packaging real power manager applications, in order to expand the honeypot applied range.

2017-02-23
Jia, L., Sen, S., Garg, D., Datta, A..  2015.  "A Logic of Programs with Interface-Confined Code". 2015 IEEE 28th Computer Security Foundations Symposium. :512–525.

Interface-confinement is a common mechanism that secures untrusted code by executing it inside a sandbox. The sandbox limits (confines) the code's interaction with key system resources to a restricted set of interfaces. This practice is seen in web browsers, hypervisors, and other security-critical systems. Motivated by these systems, we present a program logic, called System M, for modeling and proving safety properties of systems that execute adversary-supplied code via interface-confinement. In addition to using computation types to specify effects of computations, System M includes a novel invariant type to specify the properties of interface-confined code. The interpretation of invariant type includes terms whose effects satisfy an invariant. We construct a step-indexed model built over traces and prove the soundness of System M relative to the model. System M is the first program logic that allows proofs of safety for programs that execute adversary-supplied code without forcing the adversarial code to be available for deep static analysis. System M can be used to model and verify protocols as well as system designs. We demonstrate the reasoning principles of System M by verifying the state integrity property of the design of Memoir, a previously proposed trusted computing system.