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

DOI10.1007/978-3-030-81685-8_34zbMath1493.68106OpenAlexW3184432289MaRDI QIDQ832225

N. E. Zubov

Publication date: 25 March 2022

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

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Resources, concurrency, and local reasoning
• Regression verification for unbalanced recursive functions
• Modular product programs
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Dafny: An Automatic Program Verifier for Functional Correctness
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification
• Simplify: a theorem prover for program checking
• A Basis for Verifying Multi-threaded Programs
• Towards Modularly Comparing Programs Using Automated Theorem Provers
• Why3 — Where Programs Meet Provers
• Static Analysis
• \textsc{SecCSL}: security concurrent separation logic
• Property directed self composition

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