Certification of programs for secure information flow
From MaRDI portal
Publication:4134927
DOI10.1145/359636.359712zbMath0361.68033OpenAlexW2129278597MaRDI QIDQ4134927
Peter J. Denning, Dorothy E. Denning
Publication date: 1977
Published in: Communications of the ACM (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.108.995
Related Items
Automated enforcement for relaxed information release with reference points, Fast computation of strong control dependencies, Secure information flow connections, Securing interaction between threads and the scheduler in the presence of synchronization, Instruction-level security analysis for information flow in stack-based assembly languages, Hoare Logic for Disjunctive Information Flow, A secrecy-preserving language for distributed and object-oriented systems, Efficient static checker for tainted variable attacks, Type systems equivalent to data-flow analyses for imperative languages, Dynamic program slicing, Information flow control in software DB units based on formal verification, An alternative characterization of weak order dependence, Can you trust your data, Combining behavioural types with security analysis, Symbolic abstract heaps for polymorphic information-flow guard inference, Stepwise refinement of heap-manipulating code in Chalice, Fast and incremental computation of weak control closure, Efficient computation of arbitrary control dependencies, Survey on JavaScript security policies and their enforcement mechanisms in a web browser, Flexible dynamic information flow control in the presence of exceptions, Formal verification of side-channel countermeasures using self-composition, A unifying theory of control dependence and its application to arbitrary program structures, Safe functional systems through integrity types and verified assembly, Formalizing non-interference for a simple bytecode language in Coq, Efficient Information-Flow Verification Under Speculative Execution, System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory, Secure Guarded Commands, Cryptographically-masked flows, From Exponential to Polynomial-Time Security Typing via Principal Types, Simple and efficient computation of minimal weak control closure, Optimality and condensing of information flow through linear refinement, Controlling file access with types, Unnamed Item, Content dependent information flow control, The spirit of ghost code, A security flow control algorithm and its denotational semantics correctness proof, Model-Driven Information Flow Security for Component-Based Systems, A survey of challenges for runtime verification from advanced application domains (beyond software), Securing a compiler transformation, Abstract Certification of Global Non-interference in Rewriting Logic, The enforcement of security policies for computation, Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption, Information Flow Analysis for Valued-Indexed Data Security Compartments, Non-termination and secure information flow, Secure information flow by self-composition, Abstract interpretation of operational semantics for secure information flow., Type-based information flow analysis for the \(\pi\)-calculus, Type-Based Security for Mobile Computing Integrity, Secrecy and Liveness, Combining slicing and constraint solving for validation of measurement software
