Stack-based access control and secure information flow

DOI10.1017/S0956796804005453MaRDI QIDQ4676153zbMATH OpenFDO

Authors Anindya Banerjee, David A. Naumann

Publication date 3 May 2005

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0956796804005453

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• A simple semantics and static analysis for stack inspection
• scientific article; zbMATH DE number 1693037
• Noninterference with dynamic security domains and policies
• A static type system for JVM access control
• Instruction-level security analysis for information flow in stack-based assembly languages

Cited in

(23)

• Specification and static enforcement of scheduler-independent noninterference in a middleweight Java
• Noninterference in a predicative polymorphic calculus for access control
• Instruction-level security analysis for information flow in stack-based assembly languages
• Formal verification of side-channel countermeasures using self-composition
• scientific article; zbMATH DE number 1693037 (Why is no real title available?)
• Roles, stacks, histories: a triple for Hoare
• Relational decomposition
• Runtime access control in C 3.0 using extension methods
• Securing distributed .NET applications using advanced runtime access control
• Noninterference with dynamic security domains and policies
• Typing access control and secure information flow in sessions
• Interfaces for stack inspection
• scientific article; zbMATH DE number 1931734 (Why is no real title available?)
• A simple semantics and static analysis for stack inspection
• A static type system for JVM access control
• A certified lightweight non-interference Java bytecode verifier
• Runtime access control in C\(\#\)
• Secure the clones. Static enforcement of policies for secure object copying
• Relational bytecode correlations
• Secure information flow and program logics
• Towards imperative modules: reasoning about invariants and sharing of mutable state
• Observational purity and encapsulation
• Formalizing non-interference for a simple bytecode language in Coq

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Stack-based access control and secure information flow

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