Abstract Certification of Global Non-interference in Rewriting Logic

DOI10.1007/978-3-642-17071-3_6MaRDI QIDQ3066121zbMATH OpenOpenAlexWikidataFDO

Authors Mauricio Alba-Castro, Santiago Escobar, María Alpuente

Publication date 8 January 2011

Published in Formal Methods for Components and Objects (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1006.4304

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: Non-interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this paper, we present a novel security model for global non-interference which approximates non-interference as a safety property. We also propose a certification technique for global non-interference of complete Java classes based on rewriting logic, a very general logical and semantic framework that is efficiently implemented in the high-level programming language Maude. Starting from an existing Java semantics specification written in Maude, we develop an extended, information-flow Java semantics that allows us to correctly observe global non-interference policies. In order to achieve a finite state transition system, we develop an abstract Java semantics that we use for secure and effective non-interference Java analysis. The analysis produces certificates that are independently checkable and are small enough to be used in practice.

Recommendations

• scientific article; zbMATH DE number 1617312
• A proof system for abstract non-interference
• Rewriting logic as a framework for generic verification tools
• A Verification Logic for Rewriting Logic
• Certifying proofs in the first-order theory of rewriting
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Abstract non-interference
• Formal verification of language-based concurrent noninterference
• Symbolic algorithmic verification of intransitive generalized noninterference

Cites work

• A logic for information flow in object-oriented programs
• Abstract interpretation of operational semantics for secure information flow.
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Certification of programs for secure information flow
• scientific article; zbMATH DE number 1948407 (Why is no real title available?)
• Justification logic and history based computation
• On flow-sensitive security types
• Systematic design of program transformation frameworks by abstract interpretation
• The rewriting logic semantics project

Cited in

(6)

• Twenty years of rewriting logic
• The rewriting logic semantics project: a progress report
• Abstract non-interference
• The rewriting logic semantics project: a progress report
• Computer Science Logic
• Debugging Maude programs via runtime assertion checking and trace slicing

Describes a project that uses

Uses Software

• Maude
• JML

This page was built for publication: Abstract Certification of Global Non-interference in Rewriting Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3066121)