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
Inlined Reference Monitors: Certification,Concurrency and Tree Based Monitoring
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
2013 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Reference monitor inlining is a technique for enforcing security policies by injecting security checks into the untrusted software in a style similar to aspect-oriented programming. The intention is that the injected code enforces compliance with the policy (security), without adding behavior (conservativity) or affecting existing policy compliant behavior (transparency).

This thesis consists of four papers which covers a range of topics including formalization of monitor inlining correctness properties, certification of inlined monitors, limitations in multithreaded settings and extensions using data-flow monitoring.

The first paper addresses the problem of having a potentially complex program rewriter as part of the trusted computing base. By means of proof-carrying code we show how the inliner can be replaced by a relatively simple proof-checker. This technique also enables the use of monitor inlining for quality assurance at development time, while minimizing the need for post-shipping code rewrites.

The second paper focuses on the issues associated with monitor inlining in a concurrent setting. Specifically, it discusses the problem of maintaining transparency when introducing locks for synchronizing monitor state reads and updates. Due to Java's relaxed memory model, it turns out to be impossible for a monitor to be entirely transparent without sacrificing the security property. To accommodate for this, the paper proposes a set of new correctness properties shown to be realistic and realizable.

The third paper also focuses on problems due to concurrency and identifies a class of race-free policies that precisely characterizes the set of inlineable policies. This is done by showing that inlining of a policy outside this class is either not secure or not transparent, and by exhibiting a concrete algorithm for inlining of policies inside the class which is secure, conservative, and transparent. The paper also discusses how certification in the style of proof-carrying code could be supported in multithreaded Java programs.

The fourth paper formalizes a new type of data centric runtime monitoring which combines monitor inlining with taint tracking. As opposed to ordinary techniques which focus on monitoring linear flows of events, the approach presented here relies on tree shaped traces. The paper describes how the approach can be efficiently implemented and presents a denotational semantics for a simple ``while'' language illustrating how the theoretical foundations is to be used in a practical setting.

Each paper is concluded by a practical evaluation of the theoretical results, based on a prototype implementation and case studies on real-world applications and policies.

Abstract [sv]

Referensmonitorinvävning, eller monitorinvävning, är en teknik som används för att se till att en given säkerhetspolicy efterföljs under exekvering av potentiellt skadlig kod. Tekniken går ut på att bädda in en uppsättning säkerhetskontroller (en säkerhetsmonitor) i koden på ett sätt som kan jämföras med aspektorienterad programmering. Syftet med den invävda monitorn är att garantera att policyn efterföljs (säkerhet) utan att påverka ursprungsprogrammets beteende, såvida det följer policyn (transparans och konservativitet).

Denna avhandling innefattar fyra artiklar som tillsammans täcker in en rad ämnen rörande monitorinvävning. Bland annat diskuteras formalisering av korrekthetsegenskaper hos invävda monitorer, certifiering av invävda monitorer, begränsningar i multitrådade program och utökningar för hantering av dataflödesmonitorering.

Den första artikeln behandlar problemen associerade med att ha en potentiellt komplex programmodifierare som del i den säkerhetskritiska komponenten av ett datorsystem. Genom så kallad bevisbärande kod visar vi hur en monitorinvävare kan ersättas av en relativt enkel beviskontrollerare. Denna teknik möjliggör även användandet av monitorinvävning som hjälpmedel för programutvecklare och eliminerar behovet av programmodifikationer efter att programmet distribuerats.

Den andra artikeln fokuserar på problemen kring invävning av monitorer i multitrådade program. Artikeln diskuterar problemen kring att upprätthålla transparans trots införandet av lås för synkronisering av läsningar av och skrivningar till säkerhetstillståndet. På grund av Javas minnesmodell visar det sig dock omöjligt att bädda in en säkerhetsmonitor på ett säkert och transparent sätt. För att ackommodera för detta föreslås en ny uppsättning korrekthetsegenskaper som visas vara realistiska och realiserbara.

Den tredje artikeln fokuserar även den på problemen kring flertrådad exekvering och karaktäriserar en egenskap för en policy som är tillräcklig och nödvändig för att både säkerhet och transparens ska uppnås. Detta görs genom att visa att en policy utan egenskapen inte kan upprätthållas på ett säkert och transparent sätt, och genom att beskriva en implementation av en monitorinvävare som är säker och transparent för en policy som har egenskapen. Artikeln diskuterar också hur certifiering av säkerhetsmonitorer i flertrådade program kan realiseras genom bevisbärande kod.

Den fjärde artikeln beskriver en ny typ av datacentrisk säkerhetsmonitorering som kombinerar monitorinvävning med dataflödesanalys. Till skillnad mot existerande tekniker som fokuserar på linjära sekvenser av säkerhetskritiska händelser förlitar sig tekniken som presenteras här på trädformade händelsesekvenser. Artikeln beskriver hur tekniken kan implementeras på ett effektivt sätt med hjälp av abstraktion.

Varje artikel avslutas med en praktisk evaluering av de teoretiska resultaten baserat på en prototypimplementation och fallstudier av verkliga program och säkerhetsegenskaper.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2013. , viii, 20 p.
Series
Trita-CSC-A, ISSN 1653-5723 ; 2013:01
Keyword [en]
Runtime monitoring, policy enforcement, tree automata, monitor inlining, certification, concurrency
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-118486ISBN: 978-91-7501-654-2 (print)OAI: oai:DiVA.org:kth-118486DiVA: diva2:606487
Public defence
2013-03-15, F3, Lindstedtsvägen 26 Entreplan, KTH, Stockholm, 10:00 (English)
Opponent
Supervisors
Note

QC 20130220

Available from: 2013-02-20 Created: 2013-02-19 Last updated: 2013-02-20Bibliographically approved
List of papers
1. A proof carrying code framework for inlined reference monitors in java bytecode
Open this publication in new window or tab >>A proof carrying code framework for inlined reference monitors in java bytecode
2010 (English)Report (Refereed)
Abstract [en]

We propose a light-weight approach for certification of monitor inlining for sequential Java bytecode using proof-carrying code. The goal is to enable the use of monitoring for quality assurance at development time, while minimizing the need for post-shipping code rewrites as well as changes to the end-host TCB. Standard automaton-based security policies express constraints on allowed API call/return sequences. Proofs are represented as JML-style program annotations. This is adequate in our case as all proofs generated in our framework are recognized in time polynomial in the size of the program. Policy adherence is proved by comparing the transitions of an inlined monitor with those of a trusted "ghost" monitor represented using JML-style annotations. At time of receiving a program with proof annotations, it is sufficient for the receiver to plug in its own trusted ghost monitor and check the resulting verification conditions, to verify that inlining has been performed correctly, of the correct policy. We have proved correctness of the approach at the Java bytecode level and formalized the proof of soundness in Coq. An implementation, including an application loader running on a mobile device, is available, and we conclude by giving benchmarks for two sample applications.

Publisher
17 p.
National Category
Computer and Information Science
Identifiers
urn:nbn:se:kth:diva-66392 (URN)
Note

QC 20120130

Available from: 2012-01-26 Created: 2012-01-26 Last updated: 2013-02-20Bibliographically approved
2. Provably Correct Inline Monitoring for Multi-threaded Java-like Programs
Open this publication in new window or tab >>Provably Correct Inline Monitoring for Multi-threaded Java-like Programs
2010 (English)In: Journal of Computer Security, ISSN 0926-227X, E-ISSN 1875-8924, Vol. 18, no 1, 37-59 p.Article in journal (Other (popular science, discussion, etc.)) Published
Abstract [en]

Inline reference monitoring is a powerful technique to enforce security policies on untrusted programs. The security-by-contract paradigm proposed by the EU FP6 S 3 MS project uses policies, monitoring, and monitor inlining to secure third-party applications running on mobile devices. The focus of this paper is on multi-threaded Java bytecode. An important consideration is that inlining should interfere with the client program only when mandated by the security policy. In a multithreaded setting, however, this requirement turns out to be problematic. Generally, inliners use locks to control access to shared resources such as an embedded monitor state. This will interfere with application program non-determinism due to Java's relaxed memory consistency model, and rule out the transparency property, that all policy-adherent behaviour of an application program is preserved under inlining. In its place we propose a notion of strong conservativity, to formalise the property that the inliner can terminate the client program only when the policy is about to be violated. An example inlining algorithm is given and proved to be strongly conservative. Finally, benchmarks are given for four example applications studied in the S 3 MS project.

Keyword
Security-by-contract; Runtime monitoring; Monitor inlining.
National Category
Computer and Information Science
Identifiers
urn:nbn:se:kth:diva-62951 (URN)10.3233/JCS-2010-0365 (DOI)2-s2.0-71749083026 (Scopus ID)
Note
QC 20120125Available from: 2012-01-20 Created: 2012-01-20 Last updated: 2017-12-08Bibliographically approved
3. Security monitor inlining and certification for multithreaded Java
Open this publication in new window or tab >>Security monitor inlining and certification for multithreaded Java
2015 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 25, no 3, 528-565 p.Article in journal (Refereed) Published
Abstract [en]

Security monitor inlining is a technique for security policy enforcement whereby monitor functionality is injected into application code in the style of aspect-oriented programming. The intention is that the injected code enforces compliance with the policy (security), and otherwise interferes with the application as little as possible (conservativity and transparency). Such inliners are said to be correct. For sequential Java-like languages, inlining is well understood, and several provably correct inliners have been proposed. For multithreaded Java one difficulty is the need to maintain a shared monitor state. We show that this problem introduces fundamental limitations in the type of security policies that can be correctly enforced by inlining. A class of race-free policies is identified that precisely characterizes the inlineable policies by showing that inlining of a policy outside this class is either not secure or not transparent, and by exhibiting a concrete inliner for policies inside the class which is secure, conservative and transparent. The inliner is implemented for Java and applied to a number of practical application security policies. Finally, we discuss how certification in the style of proof-carrying code could be supported for inlined programs by using annotations to reduce a potentially complex verification problem for multithreaded Java bytecode to sequential verification of just the inlined code snippets.

Keyword
Aspect oriented programming, Codes (symbols), Computer software, Security systems, Application codes, Application security, Fundamental limitations, Java byte codes, Proof-carrying code, Security monitors, Security policy enforcement, Verification problems
National Category
Computer and Information Science
Identifiers
urn:nbn:se:kth:diva-62964 (URN)10.1017/S0960129512000916 (DOI)000348369900003 ()2-s2.0-84921923104 (Scopus ID)
Funder
EU, FP7, Seventh Framework Programme
Note

QC 20150303. Updated from submitted to published.

Available from: 2012-01-20 Created: 2012-01-20 Last updated: 2017-12-08Bibliographically approved
4. TreeDroid: A tree automaton based approach to enforcing data processing policies
Open this publication in new window or tab >>TreeDroid: A tree automaton based approach to enforcing data processing policies
2012 (English)In: CCS '12 Proceedings of the 2012 ACM conference on Computer and communications security, ACM , 2012, 894-905 p.Conference paper, Published paper (Refereed)
Abstract [en]

Current approaches to security policy monitoring are based on linear control flow constraints such as runQuery may be evaluated only after sanitize. However, realistic security policies must be able to conveniently capture data flow constraints as well. An example is a policy stating that arguments to the function runQuery must be either constants, outputs of a function sanitize, or concatenations of any such values. We present a novel approach to security policy monitoring that uses tree automata to capture constraints on the way data is processed along an execution. We present a λ-calculus based model of the framework, investigate some of the models meta-properties, and show how it can be implemented using labels corresponding to automaton states to reflect the computational histories of each data item. We show how a standard denotational semantics induces the expected monitoring regime on a simple "while" language. Finally we implement the framework for the Dalvik VM using TaintDroid as the underlying data flow tracking mechanism, and evaluate its functionality and performance on five case studies.

Place, publisher, year, edition, pages
ACM, 2012
Series
Proceedings of the ACM Conference on Computer and Communications Security, ISSN 1543-7221
Keyword
Policy enforcement, Runtime monitoring, Tree automata
National Category
Computer and Information Science
Identifiers
urn:nbn:se:kth:diva-108006 (URN)10.1145/2382196.2382290 (DOI)2-s2.0-84869424220 (Scopus ID)978-145031650-7 (ISBN)
Conference
2012 ACM Conference on Computer and Communications Security, CCS 2012, 16 October 2012 through 18 October 2012, Raleigh, NC
Funder
ICT - The Next Generation
Note

QC 20121221

Available from: 2012-12-21 Created: 2012-12-19 Last updated: 2013-04-11Bibliographically approved

Open Access in DiVA

fulltext(1170 kB)442 downloads
File information
File name FULLTEXT03.pdfFile size 1170 kBChecksum SHA-512
4caa26b0f2a8915ebc7c74c6ac9df4ce3b18257d2d78dd457068ba352164e0907dcf2fb27e24241d8166161dc120acc9832a6631cc07d80583602c8040429dcf
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Lundblad, Andreas
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 442 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 704 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