Bytecode analysis for proof carrying code

Martin Wildmoser; Amine Chaieb; Tobias Nipkow

doi:10.1016/j.entcs.2005.02.040

Bytecode analysis for proof carrying code

Martin Wildmoser, Amine Chaieb, Tobias Nipkow

Default

Technical University of Munich

Research output: Contribution to journal › Article › peer-review

13 Scopus citations

Abstract

Out of annotated programs proof carrying code systems construct and prove verification conditions that guarantee a given safety policy. The annotations may come from various program analyzers and must not be trusted as they need to be verified. A generic verification condition generator can be utilized such that a combination of annotations is verified incrementally. New annotations may be verified by using previously verified ones as trusted facts. We show how results from a trusted type analyzer may be combined with untrusted interval analysis to automatically verify that bytecode programs do not overflow. All trusted components are formalized and verified in Isabelle/HOL.

Original language	English
Pages (from-to)	19-34
Number of pages	16
Journal	Electronic Notes in Theoretical Computer Science
Volume	141
Issue number	1 SPEC. ISS.
DOIs	https://doi.org/10.1016/j.entcs.2005.02.040
State	Published - 5 Dec 2005

Keywords

Bytecode
Isabelle/HOL
Proof carrying code
Safety policy
Type analyzer

Access to Document

10.1016/j.entcs.2005.02.040

Cite this

@article{2d796bfc5e5c4c659b6c627e8688ce79,

title = "Bytecode analysis for proof carrying code",

abstract = "Out of annotated programs proof carrying code systems construct and prove verification conditions that guarantee a given safety policy. The annotations may come from various program analyzers and must not be trusted as they need to be verified. A generic verification condition generator can be utilized such that a combination of annotations is verified incrementally. New annotations may be verified by using previously verified ones as trusted facts. We show how results from a trusted type analyzer may be combined with untrusted interval analysis to automatically verify that bytecode programs do not overflow. All trusted components are formalized and verified in Isabelle/HOL.",

keywords = "Bytecode, Isabelle/HOL, Proof carrying code, Safety policy, Type analyzer",

author = "Martin Wildmoser and Amine Chaieb and Tobias Nipkow",

year = "2005",

month = dec,

day = "5",

doi = "10.1016/j.entcs.2005.02.040",

language = "English",

volume = "141",

pages = "19--34",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "1 SPEC. ISS.",

}

TY - JOUR

T1 - Bytecode analysis for proof carrying code

AU - Wildmoser, Martin

AU - Chaieb, Amine

AU - Nipkow, Tobias

PY - 2005/12/5

Y1 - 2005/12/5

N2 - Out of annotated programs proof carrying code systems construct and prove verification conditions that guarantee a given safety policy. The annotations may come from various program analyzers and must not be trusted as they need to be verified. A generic verification condition generator can be utilized such that a combination of annotations is verified incrementally. New annotations may be verified by using previously verified ones as trusted facts. We show how results from a trusted type analyzer may be combined with untrusted interval analysis to automatically verify that bytecode programs do not overflow. All trusted components are formalized and verified in Isabelle/HOL.

AB - Out of annotated programs proof carrying code systems construct and prove verification conditions that guarantee a given safety policy. The annotations may come from various program analyzers and must not be trusted as they need to be verified. A generic verification condition generator can be utilized such that a combination of annotations is verified incrementally. New annotations may be verified by using previously verified ones as trusted facts. We show how results from a trusted type analyzer may be combined with untrusted interval analysis to automatically verify that bytecode programs do not overflow. All trusted components are formalized and verified in Isabelle/HOL.

KW - Bytecode

KW - Isabelle/HOL

KW - Proof carrying code

KW - Safety policy

KW - Type analyzer

UR - http://www.scopus.com/inward/record.url?scp=28044446798&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2005.02.040

DO - 10.1016/j.entcs.2005.02.040

M3 - Article

AN - SCOPUS:28044446798

SN - 1571-0661

VL - 141

SP - 19

EP - 34

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 1 SPEC. ISS.

ER -

Bytecode analysis for proof carrying code

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this