Program synthesis for interactive-security systems

DOI10.1007/s10703-017-0296-5zbMath1386.68032OpenAlexW2755381580MaRDI QIDQ1696589

Sanjit A. Seshia, William R. Harris, Somesh Jha, Thomas W. Reps

Publication date: 14 February 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://escholarship.org/uc/item/8h27h8sb

zbMATH Keywords

computer securityprogram synthesisinformation flowcapabilitiessecure isolated regions

Mathematics Subject Classification ID

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

Uses Software

• LLVM
• JFlow
• Privtrans
• SGX
• Merlin
• Laminar
• VC3
• EROS
• Moat
• Fable
• F*

Cites Work

• Laminar
• Efficient secure two-party protocols. Techniques and constructions
• Modular strategies for recursive game graphs
• Towards fully automatic placement of security sanitizers and declassifiers
• Visibly pushdown languages
• A lattice model of secure information flow
• Secure distributed programming with value-dependent types
• Probabilistic relational verification for cryptographic implementations
• Computer Aided Verification

This page was built for publication: Program synthesis for interactive-security systems