Product programs in the wild: retrofitting program verifiers to check information flow security

DOI10.1007/978-3-030-81685-8_34MaRDI QIDQ832225zbMATH OpenOpenAlexFDO

Authors N. E. Zubov

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-81685-8_34

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Modular product programs
• Product programs and relational program logics
• Beyond 2-safety: asymmetric product programs for relational program verification
• Lazy self-composition for security verification
• scientific article; zbMATH DE number 2104621

Cites work

• scientific article; zbMATH DE number 7561456 (Why is no real title available?)
• A Basis for Verifying Multi-threaded Programs
• Beyond 2-safety: asymmetric product programs for relational program verification
• Dafny: an automatic program verifier for functional correctness
• Modular product programs
• Property directed self composition
• Regression verification for unbalanced recursive functions
• Resources, concurrency, and local reasoning
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Simplify: a theorem prover for program checking
• Static Analysis
• Towards modularly comparing programs using automated theorem provers
• Viper: a verification infrastructure for permission-based reasoning
• Why3 -- where programs meet provers
• \textsc{SecCSL}: security concurrent separation logic

Cited in

(3)

• scientific article; zbMATH DE number 1808257 (Why is no real title available?)
• Lazy self-composition for security verification
• Is Your Software on Dope?

Describes a project that uses

Uses Software

• Dafny
• KRAKATOA
• Why3
• Caduceus
• Frama-C
• z3
• SIMPLIFY
• VCC
• Chalice
• Boogie
• WhyML
• VerCors
• GPUVerify
• SymDiff
• Viper
• Jif
• RVT
• Nagini

This page was built for publication: Product programs in the wild: retrofitting program verifiers to check information flow security

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