Cryptographically Assured Information Flow: Assured Remote Execution
- URL: http://arxiv.org/abs/2402.02630v1
- Date: Sun, 4 Feb 2024 22:47:03 GMT
- Title: Cryptographically Assured Information Flow: Assured Remote Execution
- Authors: Scott L. Dyer, Christian A. Femrite, Joshua D. Guttman, Julian P. Lanson, Moses D. Liskov,
- Abstract summary: Assured Remote Execution on a device is the ability of suitably authorized parties to construct secure channels with known processes.
We show that a simple hardware-level mechanism called Cryptographically Assured Information Flow (CAIF) enables Assured Remote Execution.
- Score: 0.0
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Assured Remote Execution on a device is the ability of suitably authorized parties to construct secure channels with known processes -- i.e. processes executing known code -- running on it. Assured Remote Execution requires a hardware basis including cryptographic primitives. In this paper, we show that a simple hardware-level mechanism called Cryptographically Assured Information Flow (CAIF) enables Assured Remote Execution. CAIF is akin to some operations in existing Trusted Execution Environments, but securely implements an ideal functionality defined in terms of logging and confidential escrow. We show how to achieve Assured Remote Execution for a wide variety of processes on a CAIF device. Cryptographic protocol analysis demonstrates our security goals are achieved even against a strong adversary that may modify our programs and execute unauthorized programs on the device. Assured Remote Execution enables useful functionality such as trustworthy remote attestation, and provides some of the support needed for secure remote reprogramming.
Related papers
- TRACES: TEE-based Runtime Auditing for Commodity Embedded Systems [9.32090482996659]
Control Flow Auditing (CFA) offers a means to detect control flow hijacking attacks on remote devices.
CFA generates a trace (CFLog) containing the destination of all branching instructions executed.
TraCES guarantees reliable delivery of periodic runtime reports even when Prv is compromised.
arXiv Detail & Related papers (2024-09-27T20:10:43Z) - SISSA: Real-time Monitoring of Hardware Functional Safety and
Cybersecurity with In-vehicle SOME/IP Ethernet Traffic [49.549771439609046]
We propose SISSA, a SOME/IP communication traffic-based approach for modeling and analyzing in-vehicle functional safety and cyber security.
Specifically, SISSA models hardware failures with the Weibull distribution and addresses five potential attacks on SOME/IP communication.
Extensive experimental results show the effectiveness and efficiency of SISSA.
arXiv Detail & Related papers (2024-02-21T03:31:40Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure.
This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus.
We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
arXiv Detail & Related papers (2024-01-19T14:52:04Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs)
TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks.
We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
arXiv Detail & Related papers (2024-01-17T00:56:23Z) - Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
We advocate using secure program partitioning to synthesize cryptographic applications.
This approach is promising, but formal results for the security of such compilers are limited in scope.
We develop a compiler security proof that handles subtleties essential for robust, efficient applications.
arXiv Detail & Related papers (2024-01-06T02:57:44Z) - Attestation with Constrained Relying Party [0.7249731529275341]
We show that our protocol, including the needed cryptography and message processing, can be implemented with a code size of 6 KB.
We show that our protocol, including the needed cryptography and message processing, can be implemented with a code size of 6 KB and validate its security via model checking with the ProVerif tool.
arXiv Detail & Related papers (2023-12-14T13:05:21Z) - Poster: Control-Flow Integrity in Low-end Embedded Devices [12.193184827858326]
This work constructs an architecture that ensures integrity of software execution against run-time attacks.
It is built atop a recently proposed CASU -- a low-cost active Root-of-Trust (RoT) that guarantees software immutability.
arXiv Detail & Related papers (2023-09-19T07:52:43Z) - A Novel Approach to Identify Security Controls in Source Code [4.598579706242066]
This paper enumerates a comprehensive list of commonly used security controls and creates a dataset for each one of them.
It uses the state-of-the-art NLP technique Bidirectional Representations from Transformers (BERT) and the Tactic Detector from our prior work to show that security controls could be identified with high confidence.
arXiv Detail & Related papers (2023-07-10T21:14:39Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers.
We then present the pointwise feasibility conditions of the resulting safety controller.
We use these conditions to devise an event-triggered online data collection strategy.
arXiv Detail & Related papers (2022-08-23T05:02:09Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
We present a Symbolic Reinforcement Learning (SRL) based architecture for safety control of Radio Access Network (RAN) applications.
We provide a purely automated procedure in which a user can specify high-level logical safety specifications for a given cellular network topology.
We introduce a user interface (UI) developed to help a user set intent specifications to the system, and inspect the difference in agent proposed actions.
arXiv Detail & Related papers (2021-06-03T16:45:40Z) - Symbolic Reinforcement Learning for Safe RAN Control [62.997667081978825]
We show a Symbolic Reinforcement Learning (SRL) architecture for safe control in Radio Access Network (RAN) applications.
In our tool, a user can select a high-level safety specifications expressed in Linear Temporal Logic (LTL) to shield an RL agent running in a given cellular network.
We demonstrate the user interface (UI) helping the user set intent specifications to the architecture and inspect the difference in allowed and blocked actions.
arXiv Detail & Related papers (2021-03-11T10:56:49Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.