Program synthesis for interactive-security systems

DOI10.1007/S10703-017-0296-5MaRDI QIDQ1696589zbMATH OpenOpenAlexFDO

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

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

information flowcomputer securityprogram synthesiscapabilitiessecure isolated regions

Mathematics Subject Classification ID

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

Recommendations

• From program verification to program synthesis
• Programmable program synthesis
• Look for the proof to find the program: decorated-component-based program synthesis
• Synthesis with abstract examples
• Abstraction-based interaction model for synthesis

Cites work

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

Cited in

(1)

• Automated synthesis of secure platform mappings

Describes a project that uses

Uses Software

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

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

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