Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Provably correct runtime monitoring (extended abstract)
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2008 (English)In: Fm 2008: Formal Methods, Proceedings / [ed] Cuellar, J; Maibaum, T; Sere, K, 2008, Vol. 5014, 262-277 p.Conference paper, Published paper (Refereed)
Abstract [en]

Runtime monitoring is an established technique for enforcing a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has an instance of the given monitor embedded into it, which yields state changes at prescribed points according to the monitor's transition function. As our main application of these results we describe a concrete inliner, and use the annotation scheme to characterize its correctness. For this inliner, correctness of the level II annotations can be decided efficiently by a weakest precondition annotation checker, thus allowing on-device checking of inlining correctness in a proof-carrying code setting.

Place, publisher, year, edition, pages
2008. Vol. 5014, 262-277 p.
Series
Lecture Notes In Computer Science, ISSN 0302-9743 ; 5014
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-38138DOI: 10.1007/978-3-540-68237-0_19ISI: 000256247100019Scopus ID: 2-s2.0-47249101556ISBN: 978-3-540-68235-6 (print)OAI: oai:DiVA.org:kth-38138DiVA: diva2:436062
Conference
15th International Symposium on Formal Methods Location: Turku, FINLAND Date: MAY 26-30, 2008
Available from: 2011-08-22 Created: 2011-08-22 Last updated: 2012-01-20Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Dam, MadsGurov, Dilian

Search in DiVA

By author/editor
Aktug, IremDam, MadsGurov, Dilian
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 73 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf