Automated techniques for provably safe mobile code.

DOI10.1016/S0304-3975(01)00201-8MaRDI QIDQ1853627zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 21 January 2003

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(01)00201-8

zbMATH Keywords

Proof-carrying codeType systemsCertifying compilersType safetyTyped assembly language

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• Logic Programming
• scientific article; zbMATH DE number 1330435
• scientific article; zbMATH DE number 2110618
• Verification, Model Checking, and Abstract Interpretation
• Abstraction-carrying code: a model for mobile code safety

Cites work

• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 1392299 (Why is no real title available?)
• scientific article; zbMATH DE number 1420794 (Why is no real title available?)
• A dependently typed assembly language
• A framework for defining logics
• A semantic model of types and machine instructions for proof-carrying code
• A type system for expressive security policies
• Elf: A meta-language for deductive systems
• Logical frameworks
• On equivalence and canonical forms in the LF type theory
• Resource bound certification
• Stack-based typed assembly language
• Stack-based typed assembly language

Cited in

(11)

• Lazy mobile intruders
• Secure Prolog-based mobile code
• Grail: a functional form for imperative mobile code
• A type system for expressive security policies
• scientific article; zbMATH DE number 2080177 (Why is no real title available?)
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 1612498 (Why is no real title available?)
• A confinement criterion for securely executing mobile code
• Matching in security-by-contract for mobile code
• Commanding a robot in a safe way
• Proving the correctness of mobile Java code

Describes a project that uses

Uses Software

• TALx86
• TIL
• Elf
• Twelf

This page was built for publication: Automated techniques for provably safe mobile code.

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