Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems

• URL: http://arxiv.org/abs/2309.09141v1
• Date: Sun, 17 Sep 2023 02:57:05 GMT
• Title: Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems
• Authors: Yongwang Zhao, David Sanan, Fuyuan Zhang, Yang Liu
• Abstract summary: We propose a rely-guarantee-based compositional reasoning approach for information-flow security (IFS) for concurrent systems. We first design a language by incorporating Event'' into concurrent languages and give the IFS semantics of the language. For compositional reasoning of IFS, we use rely-guarantee specification to define new forms of unwinding conditions (UCs) on events.
• Score: 5.965840906609809
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: High assurance of information-flow security (IFS) for concurrent systems is challenging. A promising way for formal verification of concurrent systems is the rely-guarantee method. However, existing compositional reasoning approaches for IFS concentrate on language-based IFS. It is often not applicable for system-level security, such as multicore operating system kernels, in which secrecy of actions should also be considered. On the other hand, existing studies on the rely-guarantee method are basically built on concurrent programming languages, by which semantics of concurrent systems cannot be completely captured in a straightforward way. In order to formally verify state-action based IFS for concurrent systems, we propose a rely-guarantee-based compositional reasoning approach for IFS in this paper. We first design a language by incorporating ``Event'' into concurrent languages and give the IFS semantics of the language. As a primitive element, events offer an extremely neat framework for modeling system and are not necessarily atomic in our language. For compositional reasoning of IFS, we use rely-guarantee specification to define new forms of unwinding conditions (UCs) on events, i.e., event UCs. By a rely-guarantee proof system of the language and the soundness of event UCs, we have that event UCs imply IFS of concurrent systems. In such a way, we relax the atomicity constraint of actions in traditional UCs and provide a compositional reasoning way for IFS in which security proof of systems can be discharged by independent security proof on individual events. Finally, we mechanize the approach in Isabelle/HOL and develop a formal specification and its IFS proof for multicore separation kernels as a study case according to an industrial standard -- ARINC 653.

Related papers

• Uni-Sign: Toward Unified Sign Language Understanding at Scale [90.76641997060513]
  We propose a unified pre-training framework that eliminates the gap between pre-training and downstream SLU tasks. Uni-Sign achieves state-of-the-art performance across multiple downstream SLU tasks.
  arXiv  Detail & Related papers  (2025-01-25T11:51:23Z)
• WIP: An Engaging Undergraduate Intro to Model Checking in Software Engineering Using TLA+ [0.358439716487063]
  We aim to qualitatively assess the state of formal methods in computer science programs. We construct level-appropriate examples that could be included midway into one's undergraduate studies.
  arXiv  Detail & Related papers  (2024-07-30T19:31:14Z)
• Beyond Mask: Rethinking Guidance Types in Few-shot Segmentation [67.35274834837064]
  We develop a universal vision-language framework (UniFSS) to integrate prompts from text, mask, box, and image. UniFSS significantly outperforms the state-of-the-art methods.
  arXiv  Detail & Related papers  (2024-07-16T08:41:01Z)
• SCIF: A Language for Compositional Smart Contract Security [3.2707122129201975]
  We introduce SCIF, a language for building smart contracts that are compositionally secure. SCIF is based on the fundamentally compositional principle of secure information flow. It supports a rich ecosystem of interacting principals with partial trust.
  arXiv  Detail & Related papers  (2024-07-01T11:51:21Z)
• Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications [0.0]
  This article proposes PiCore, a rely-guarantee reasoning framework for formal specification and verification of CRSs. We design an event specification language supporting complex reaction structures and its rely-guarantee proof system to detach the specification and logic of reactive aspects of CRSs from event behaviours. By this design, we have successfully integrated two existing languages and their rely-guarantee proof systems without any change of their specification and proofs.
  arXiv  Detail & Related papers  (2023-09-17T03:43:25Z)
• (Security) Assertions by Large Language Models [25.270188328436618]
  We investigate the use of emerging large language models (LLMs) for code generation in hardware assertion generation for security. We focus our attention on a popular LLM and characterize its ability to write assertions out of the box, given varying levels of detail in the prompt.
  arXiv  Detail & Related papers  (2023-06-24T17:44:36Z)
• Token-level Sequence Labeling for Spoken Language Understanding using Compositional End-to-End Models [94.30953696090758]
  We build compositional end-to-end spoken language understanding systems. By relying on intermediate decoders trained for ASR, our end-to-end systems transform the input modality from speech to token-level representations. Our models outperform both cascaded and direct end-to-end models on a labeling task of named entity recognition.
  arXiv  Detail & Related papers  (2022-10-27T19:33:18Z)
• 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)
• Generalized Few-shot Semantic Segmentation [68.69434831359669]
  We introduce a new benchmark called Generalized Few-Shot Semantic (GFS-Seg) to analyze the ability of simultaneously segmenting the novel categories. It is the first study showing that previous representative state-of-the-art generalizations fall short in GFS-Seg. We propose the Context-Aware Prototype Learning (CAPL) that significantly improves performance by 1) leveraging the co-occurrence prior knowledge from support samples, and 2) dynamically enriching contextual information to the conditioned, on the content of each query image.
  arXiv  Detail & Related papers  (2020-10-11T10:13:21Z)
• PIN: A Novel Parallel Interactive Network for Spoken Language Understanding [68.53121591998483]
  In the existing RNN-based approaches, ID and SF tasks are often jointly modeled to utilize the correlation information between them. The experiments on two benchmark datasets, i.e., SNIPS and ATIS, demonstrate the effectiveness of our approach. More encouragingly, by using the feature embedding of the utterance generated by the pre-trained language model BERT, our method achieves the state-of-the-art among all comparison approaches.
  arXiv  Detail & Related papers  (2020-09-28T15:59:31Z)
• Quantifying Assurance in Learning-enabled Systems [3.0938904602244355]
  Dependability assurance of systems embedding machine learning components is a key step for their use in safety-critical applications. This paper develops a quantitative notion of assurance that an LES is dependable, as a core component of its assurance case. We illustrate the utility of assurance measures by application to a real world autonomous aviation system.
  arXiv  Detail & Related papers  (2020-06-18T08:11:50Z)

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.