A Functional Scenario for Bytecode Verification of Resource Bounds
Identifieur interne : 006F67 ( Main/Merge ); précédent : 006F66; suivant : 006F68A Functional Scenario for Bytecode Verification of Resource Bounds
Auteurs : Roberto M. Amadio [France] ; Solange Coupet-Grimal [France] ; Silvano Dal Zilio [France] ; Line Jakubiec [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We consider a scenario where (functional) programs in pre-compiled form are exchanged among untrusted parties. Our contribution is a system of annotations for the code that can be verified at load time so as to ensure bounds on the time and space resources required for its execution, as well as to guarantee the usual integrity properties. Specifically, we define a simple stack machine for a first-order functional language and show how to perform type, size, and termination verifications at the level of the bytecode of the machine. In particular, we show that a combination of size verification based on quasi-interpretations and of termination verification based on lexicographic path orders leads to an explicit bound on the space required for the execution.
Url:
DOI: 10.1007/978-3-540-30124-0_22
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000199
- to stream Istex, to step Curation: 000198
- to stream Istex, to step Checkpoint: 001872
Links to Exploration step
ISTEX:094BDC28B9E14B9871C0994CCDA6981B154EA12FLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Functional Scenario for Bytecode Verification of Resource Bounds</title><author><name sortKey="Amadio, Roberto M" sort="Amadio, Roberto M" uniqKey="Amadio R" first="Roberto M." last="Amadio">Roberto M. Amadio</name></author><author><name sortKey="Coupet Grimal, Solange" sort="Coupet Grimal, Solange" uniqKey="Coupet Grimal S" first="Solange" last="Coupet-Grimal">Solange Coupet-Grimal</name></author><author><name sortKey="Dal Zilio, Silvano" sort="Dal Zilio, Silvano" uniqKey="Dal Zilio S" first="Silvano" last="Dal Zilio">Silvano Dal Zilio</name></author><author><name sortKey="Jakubiec, Line" sort="Jakubiec, Line" uniqKey="Jakubiec L" first="Line" last="Jakubiec">Line Jakubiec</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:094BDC28B9E14B9871C0994CCDA6981B154EA12F</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1007/978-3-540-30124-0_22</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-10HVCNCX-P/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000199</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000199</idno><idno type="wicri:Area/Istex/Curation">000198</idno><idno type="wicri:Area/Istex/Checkpoint">001872</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001872</idno><idno type="wicri:doubleKey">0302-9743:2004:Amadio R:a:functional:scenario</idno><idno type="wicri:Area/Main/Merge">006F67</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Functional Scenario for Bytecode Verification of Resource Bounds</title><author><name sortKey="Amadio, Roberto M" sort="Amadio, Roberto M" uniqKey="Amadio R" first="Roberto M." last="Amadio">Roberto M. Amadio</name><affiliation wicri:level="4"><orgName type="university">Université de Provence</orgName><country>France</country><placeName><settlement type="city">Marseille</settlement><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region></placeName></affiliation></author><author><name sortKey="Coupet Grimal, Solange" sort="Coupet Grimal, Solange" uniqKey="Coupet Grimal S" first="Solange" last="Coupet-Grimal">Solange Coupet-Grimal</name><affiliation wicri:level="4"><orgName type="university">Université de Provence</orgName><country>France</country><placeName><settlement type="city">Marseille</settlement><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region></placeName></affiliation></author><author><name sortKey="Dal Zilio, Silvano" sort="Dal Zilio, Silvano" uniqKey="Dal Zilio S" first="Silvano" last="Dal Zilio">Silvano Dal Zilio</name><affiliation wicri:level="4"><orgName type="university">Université de Provence</orgName><country>France</country><placeName><settlement type="city">Marseille</settlement><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region></placeName></affiliation></author><author><name sortKey="Jakubiec, Line" sort="Jakubiec, Line" uniqKey="Jakubiec L" first="Line" last="Jakubiec">Line Jakubiec</name><affiliation wicri:level="4"><orgName type="university">Université de Provence</orgName><country>France</country><placeName><settlement type="city">Marseille</settlement><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region></placeName></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We consider a scenario where (functional) programs in pre-compiled form are exchanged among untrusted parties. Our contribution is a system of annotations for the code that can be verified at load time so as to ensure bounds on the time and space resources required for its execution, as well as to guarantee the usual integrity properties. Specifically, we define a simple stack machine for a first-order functional language and show how to perform type, size, and termination verifications at the level of the bytecode of the machine. In particular, we show that a combination of size verification based on quasi-interpretations and of termination verification based on lexicographic path orders leads to an explicit bound on the space required for the execution.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006F67 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 006F67 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= ISTEX:094BDC28B9E14B9871C0994CCDA6981B154EA12F
|texte= A Functional Scenario for Bytecode Verification of Resource Bounds
}}
| This area was generated with Dilib version V0.6.33. |  |