A Functional Scenario for Bytecode Verification of Resource Bounds
Identifieur interne : 000199 ( Istex/Corpus ); précédent : 000198; suivant : 000200A Functional Scenario for Bytecode Verification of Resource Bounds
Auteurs : Roberto M. Amadio ; Solange Coupet-Grimal ; Silvano Dal Zilio ; Line JakubiecSource :
- 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 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><affiliation><mods:affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </mods:affiliation></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><mods:affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </mods:affiliation></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><mods:affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </mods:affiliation></affiliation></author><author><name sortKey="Jakubiec, Line" sort="Jakubiec, Line" uniqKey="Jakubiec L" first="Line" last="Jakubiec">Line Jakubiec</name><affiliation><mods:affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </mods:affiliation></affiliation></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></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><mods:affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </mods:affiliation></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><mods:affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </mods:affiliation></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><mods:affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </mods:affiliation></affiliation></author><author><name sortKey="Jakubiec, Line" sort="Jakubiec, Line" uniqKey="Jakubiec L" first="Line" last="Jakubiec">Line Jakubiec</name><affiliation><mods:affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </mods:affiliation></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><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Roberto M. Amadio</name><affiliations><json:string>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence,</json:string></affiliations></json:item><json:item><name>Solange Coupet-Grimal</name><affiliations><json:string>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence,</json:string></affiliations></json:item><json:item><name>Silvano Dal Zilio</name><affiliations><json:string>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence,</json:string></affiliations></json:item><json:item><name>Line Jakubiec</name><affiliations><json:string>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence,</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-10HVCNCX-P</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><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.</abstract><qualityIndicators><score>8.464</score><pdfWordCount>8518</pdfWordCount><pdfCharCount>37328</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>122</abstractWordCount><abstractCharCount>775</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>A Functional Scenario for Bytecode Verification of Resource Bounds</title><chapterId><json:string>22</json:string><json:string>Chap22</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>2004</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>David Hutchison</name><affiliations><json:string>Lancaster University, UK</json:string></affiliations></json:item><json:item><name>Takeo Kanade</name><affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string></affiliations></json:item><json:item><name>Josef Kittler</name><affiliations><json:string>University of Surrey, Guildford, UK</json:string></affiliations></json:item><json:item><name>Jon M. Kleinberg</name><affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string></affiliations></json:item><json:item><name>Friedemann Mattern</name><affiliations><json:string>ETH Zurich, Switzerland</json:string></affiliations></json:item><json:item><name>John C. Mitchell</name><affiliations><json:string>Stanford University, CA, USA</json:string></affiliations></json:item><json:item><name>Moni Naor</name><affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string></affiliations></json:item><json:item><name>Oscar Nierstrasz</name><affiliations><json:string>University of Bern, Switzerland</json:string></affiliations></json:item><json:item><name>C. Pandu Rangan</name><affiliations><json:string>Indian Institute of Technology, Madras, India</json:string></affiliations></json:item><json:item><name>Bernhard Steffen</name><affiliations><json:string>University of Dortmund, Germany</json:string></affiliations></json:item><json:item><name>Madhu Sudan</name><affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string></affiliations></json:item><json:item><name>Demetri Terzopoulos</name><affiliations><json:string>New York University, NY, USA</json:string></affiliations></json:item><json:item><name>Dough Tygar</name><affiliations><json:string>University of California, Berkeley, CA, USA</json:string></affiliations></json:item><json:item><name>Moshe Y. Vardi</name><affiliations><json:string>Rice University, Houston, TX, USA</json:string></affiliations></json:item><json:item><name>Gerhard Weikum</name><affiliations><json:string>Max-Planck Institute of Computer Science, Saarbruecken, Germany</json:string></affiliations></json:item></editor></serie><host><title>Computer Science Logic</title><language><json:string>unknown</json:string></language><copyrightDate>2004</copyrightDate><doi><json:string>10.1007/b100120</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-540-30124-0</json:string></eisbn><bookId><json:string>978-3-540-30124-0</json:string></bookId><isbn><json:string>978-3-540-23024-3</json:string></isbn><volume>3210</volume><pages><first>265</first><last>279</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Jerzy Marcinkowski</name><affiliations><json:string>Wroclaw University,</json:string><json:string>E-mail: Jerzy.Marcinkowski@ii.uni.wroc.pl</json:string></affiliations></json:item><json:item><name>Andrzej Tarlecki</name><affiliations><json:string>Polish Academy of Sciences, Institute of Computer Science,</json:string><json:string>E-mail: tarlecki@mimuw.edu.pl</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-10HVCNCX-P</json:string></ark><publicationDate>2004</publicationDate><copyrightDate>2004</copyrightDate><doi><json:string>10.1007/978-3-540-30124-0_22</json:string></doi><id>094BDC28B9E14B9871C0994CCDA6981B154EA12F</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-10HVCNCX-P/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-10HVCNCX-P/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-10HVCNCX-P/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">A Functional Scenario for Bytecode Verification of Resource Bounds</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2004">2004</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Functional Scenario for Bytecode Verification of Resource Bounds</title><author><persName><forename type="first">Roberto</forename><forename type="first">M.</forename><surname>Amadio</surname></persName><affiliation><orgName type="department">Laboratoire d’Informatique Fondamentale de Marseille (LIF)</orgName><orgName type="institution">CNRS and Université de Provence</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Solange</forename><surname>Coupet-Grimal</surname></persName><affiliation><orgName type="department">Laboratoire d’Informatique Fondamentale de Marseille (LIF)</orgName><orgName type="institution">CNRS and Université de Provence</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Silvano</forename><nameLink>Dal</nameLink><surname>Zilio</surname></persName><affiliation><orgName type="department">Laboratoire d’Informatique Fondamentale de Marseille (LIF)</orgName><orgName type="institution">CNRS and Université de Provence</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Line</forename><surname>Jakubiec</surname></persName><affiliation><orgName type="department">Laboratoire d’Informatique Fondamentale de Marseille (LIF)</orgName><orgName type="institution">CNRS and Université de Provence</orgName><address><country key=""></country></address></affiliation></author><idno type="istex">094BDC28B9E14B9871C0994CCDA6981B154EA12F</idno><idno type="ark">ark:/67375/HCB-10HVCNCX-P</idno><idno type="DOI">10.1007/978-3-540-30124-0_22</idno></analytic><monogr><title level="m" type="main">Computer Science Logic</title><title level="m" type="sub">18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004. Proceedings</title><title level="m" type="part">Regular Papers</title><idno type="DOI">10.1007/b100120</idno><idno type="book-id">978-3-540-30124-0</idno><idno type="ISBN">978-3-540-23024-3</idno><idno type="eISBN">978-3-540-30124-0</idno><idno type="chapter-id">Chap22</idno><idno type="part-id">Part2</idno><editor><persName><forename type="first">Jerzy</forename><surname>Marcinkowski</surname></persName><email>Jerzy.Marcinkowski@ii.uni.wroc.pl</email><affiliation><orgName type="institution">Wroclaw University</orgName><address><country key=""></country></address></affiliation></editor><editor><persName><forename type="first">Andrzej</forename><surname>Tarlecki</surname></persName><email>tarlecki@mimuw.edu.pl</email><affiliation><orgName type="department">Polish Academy of Sciences</orgName><orgName type="institution">Institute of Computer Science</orgName><address><country key=""></country></address></affiliation></editor><imprint><biblScope unit="vol">3210</biblScope><biblScope unit="page" from="265">265</biblScope><biblScope unit="page" to="279">279</biblScope><biblScope unit="chapter-count">38</biblScope><biblScope unit="part-chapter-count">33</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">David</forename><surname>Hutchison</surname></persName><affiliation><orgName type="institution">Lancaster University</orgName><address><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation><orgName type="institution">Carnegie Mellon University</orgName><address><settlement>Pittsburgh</settlement><region>PA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation><orgName type="institution">University of Surrey</orgName><address><settlement>Guildford</settlement><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><settlement>Ithaca</settlement><region>NY</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation><orgName type="institution">ETH Zurich</orgName><address><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation><orgName type="institution">Stanford University</orgName><address><settlement>CA</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation><orgName type="institution">Weizmann Institute of Science</orgName><address><settlement>Rehovot</settlement><country key="IL">ISRAEL</country></address></affiliation></editor><editor><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation><orgName type="institution">University of Bern</orgName><address><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation><orgName type="institution">Indian Institute of Technology</orgName><address><settlement>Madras</settlement><country key="IN">INDIA</country></address></affiliation></editor><editor><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation><orgName type="institution">University of Dortmund</orgName><address><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation><orgName type="institution">Massachusetts Institute of Technology</orgName><address><settlement>MA</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation><orgName type="institution">New York University</orgName><address><settlement>NY</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Dough</forename><surname>Tygar</surname></persName><affiliation><orgName type="institution">University of California</orgName><address><settlement>Berkeley</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation><orgName type="institution">Rice University</orgName><address><settlement>Houston</settlement><region>TX</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation><orgName type="institution">Max-Planck Institute of Computer Science</orgName><address><settlement>Saarbruecken</settlement><country key="DE">GERMANY</country></address></affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>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.</p><p>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.</p></abstract><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-1">Mathematical Logic and Formal Languages</term></item><label>I21017</label><item><term type="Secondary" subtype="priority-2">Artificial Intelligence (incl. Robotics)</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-3">Logics and Meanings of Programs</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-10HVCNCX-P/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Dough</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName><OrgAddress><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName><OrgAddress><City>Guildford</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Cornell University</OrgName><OrgAddress><City>Ithaca</City><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Stanford University</OrgName><OrgAddress><City>CA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName><OrgAddress><City>Rehovot</City><Country>Israel</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgName>University of Bern</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName><OrgAddress><City>Madras</City><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName><OrgAddress><City>MA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff12"><OrgName>New York University</OrgName><OrgAddress><City>NY</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff13"><OrgName>University of California</OrgName><OrgAddress><City>Berkeley</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff14"><OrgName>Rice University</OrgName><OrgAddress><City>Houston</City><State>TX</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName><OrgAddress><City>Saarbruecken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-540-30124-0</BookID><BookTitle>Computer Science Logic</BookTitle><BookSubTitle>18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004. Proceedings</BookSubTitle><BookVolumeNumber>3210</BookVolumeNumber><BookSequenceNumber>3210</BookSequenceNumber><BookDOI>10.1007/b100120</BookDOI><BookTitleID>112162</BookTitleID><BookPrintISBN>978-3-540-23024-3</BookPrintISBN><BookElectronicISBN>978-3-540-30124-0</BookElectronicISBN><BookChapterCount>38</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I16048" Priority="1" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I21017" Priority="2" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><BookSubject Code="I1603X" Priority="3" Type="Secondary">Logics and Meanings of Programs</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Jerzy</GivenName><FamilyName>Marcinkowski</FamilyName></EditorName><Contact><Email>Jerzy.Marcinkowski@ii.uni.wroc.pl</Email></Contact></Editor><Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Andrzej</GivenName><FamilyName>Tarlecki</FamilyName></EditorName><Contact><Email>tarlecki@mimuw.edu.pl</Email></Contact></Editor><Affiliation ID="Aff16"><OrgName>Wroclaw University</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation><Affiliation ID="Aff17"><OrgDivision>Polish Academy of Sciences</OrgDivision><OrgName>Institute of Computer Science</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Regular Papers</PartTitle><PartChapterCount>33</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Computer Science Logic</BookTitle></PartContext></PartInfo><Chapter ID="Chap22" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>22</ChapterID><ChapterDOI>10.1007/978-3-540-30124-0_22</ChapterDOI><ChapterSequenceNumber>22</ChapterSequenceNumber><ChapterTitle Language="En">A Functional Scenario for Bytecode Verification of Resource Bounds</ChapterTitle><ChapterFirstPage>265</ChapterFirstPage><ChapterLastPage>279</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></ChapterCopyright><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>2</PartID><BookID>978-3-540-30124-0</BookID><BookTitle>Computer Science Logic</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff18"><AuthorName DisplayOrder="Western"><GivenName>Roberto</GivenName><GivenName>M.</GivenName><FamilyName>Amadio</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff18"><AuthorName DisplayOrder="Western"><GivenName>Solange</GivenName><FamilyName>Coupet-Grimal</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff18"><AuthorName DisplayOrder="Western"><GivenName>Silvano</GivenName><Particle>Dal</Particle><FamilyName>Zilio</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff18"><AuthorName DisplayOrder="Western"><GivenName>Line</GivenName><FamilyName>Jakubiec</FamilyName></AuthorName></Author><Affiliation ID="Aff18"><OrgDivision>Laboratoire d’Informatique Fondamentale de Marseille (LIF)</OrgDivision><OrgName>CNRS and Université de Provence</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>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.</Para><Para>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.</Para></Abstract><ArticleNote Type="Misc"><SimplePara>This work was partly supported by ACI Sécurité Informatique, project CRISS.</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>A Functional Scenario for Bytecode Verification of Resource Bounds</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>A Functional Scenario for Bytecode Verification of Resource Bounds</title></titleInfo><name type="personal"><namePart type="given">Roberto</namePart><namePart type="given">M.</namePart><namePart type="family">Amadio</namePart><affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Solange</namePart><namePart type="family">Coupet-Grimal</namePart><affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Silvano</namePart><namePart type="family">Dal Zilio</namePart><affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Line</namePart><namePart type="family">Jakubiec</namePart><affiliation>Laboratoire d’Informatique Fondamentale de Marseille (LIF), CNRS and Université de Provence, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2004</dateIssued><copyrightDate encoding="w3cdtf">2004</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract 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.</abstract><relatedItem type="host"><titleInfo><title>Computer Science Logic</title><subTitle>18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Jerzy</namePart><namePart type="family">Marcinkowski</namePart><affiliation>Wroclaw University, </affiliation><affiliation>E-mail: Jerzy.Marcinkowski@ii.uni.wroc.pl</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Andrzej</namePart><namePart type="family">Tarlecki</namePart><affiliation>Polish Academy of Sciences, Institute of Computer Science, </affiliation><affiliation>E-mail: tarlecki@mimuw.edu.pl</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2004</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic></subject><identifier type="DOI">10.1007/b100120</identifier><identifier type="ISBN">978-3-540-23024-3</identifier><identifier type="eISBN">978-3-540-30124-0</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">112162</identifier><identifier type="BookID">978-3-540-30124-0</identifier><identifier type="BookChapterCount">38</identifier><identifier type="BookVolumeNumber">3210</identifier><identifier type="BookSequenceNumber">3210</identifier><identifier type="PartChapterCount">33</identifier><part><date>2004</date><detail type="part"><title>Regular Papers</title></detail><detail type="volume"><number>3210</number><caption>vol.</caption></detail><extent unit="pages"><start>265</start><end>279</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2004</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>New York University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Dough</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2004</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2004</recordOrigin></recordInfo></relatedItem><identifier type="istex">094BDC28B9E14B9871C0994CCDA6981B154EA12F</identifier><identifier type="ark">ark:/67375/HCB-10HVCNCX-P</identifier><identifier type="DOI">10.1007/978-3-540-30124-0_22</identifier><identifier type="ChapterID">22</identifier><identifier type="ChapterID">Chap22</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2004</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2004</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-10HVCNCX-P/record.json</uri></json:item></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000199 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000199 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|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. |  |