Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Provably correct runtime monitoring (extended abstract)
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0001-5432-6442
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0002-0074-8786
2008 (engelsk)Inngår i: Fm 2008: Formal Methods, Proceedings / [ed] Cuellar, J; Maibaum, T; Sere, K, 2008, Vol. 5014, s. 262-277Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
2008. Vol. 5014, s. 262-277
Serie
Lecture Notes In Computer Science, ISSN 0302-9743 ; 5014
HSV kategori
Identifikatorer
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 (tryckt)OAI: oai:DiVA.org:kth-38138DiVA, id: diva2:436062
Konferanse
15th International Symposium on Formal Methods Location: Turku, FINLAND Date: MAY 26-30, 2008
Tilgjengelig fra: 2011-08-22 Laget: 2011-08-22 Sist oppdatert: 2018-01-12bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Personposter BETA

Dam, MadsGurov, Dilian

Søk i DiVA

Av forfatter/redaktør
Aktug, IremDam, MadsGurov, Dilian
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 246 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf