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
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS. KTH, Skolan för elektro- och systemteknik (EES), Centra, ACCESS Linnaeus Centre.
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS. KTH, Skolan för elektro- och systemteknik (EES), Centra, ACCESS Linnaeus Centre.ORCID-id: 0000-0001-5432-6442
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0002-0074-8786
2009 (engelsk)Inngår i: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 78, nr 5, s. 304-339Artikkel i tidsskrift (Fagfellevurdert) Published
Abstract [en]

Runtime monitoring is an established technique to enforce 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 a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.

sted, utgiver, år, opplag, sider
2009. Vol. 78, nr 5, s. 304-339
Emneord [en]
Runtime monitoring, Policy enforcement, Monitor inlining, Proof-carrying code
HSV kategori
Identifikatorer
URN: urn:nbn:se:kth:diva-13473DOI: 10.1016/j.jlap.2008.12.002ISI: 000266671300004Scopus ID: 2-s2.0-67349154073OAI: oai:DiVA.org:kth-13473DiVA, id: diva2:325502
Merknad
QC 20100618Tilgjengelig fra: 2010-06-18 Laget: 2010-06-18 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
I samme tidsskrift
Journal of Logic and Algebraic Programming

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 678 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