Safe Collaboration in Extensible Operating Systems: A Study on Real-Time Extensions

This article proposes a solution to guarantee safe interaction to components that are willing to collaborate in an extensible operating system, dedicated to small embedded systems such as smart cards, that guarantees isolation. We propose a simple way to verify the behaviour of some components using...

Full description

Saved in:
Bibliographic Details
Published in:International journal of computers & applications 2005-01, Vol.27 (1), p.20-26
Main Authors: Deville, D., Hodique, Y., Simplot-Ryl, I.
Format: Article
Language:English
Subjects:
embedded systems
Exokernel
safe extensibility
static analysis
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This article proposes a solution to guarantee safe interaction to components that are willing to collaborate in an extensible operating system, dedicated to small embedded systems such as smart cards, that guarantees isolation. We propose a simple way to verify the behaviour of some components using an extension of the type system by adding information about argument-passing modes to the method signatures (e.g., is an argument read or written?). We present a formalization of a PCC-like algorithm (off-card proof generator and on-card proof verifier) to statically check the passing modes of the components in the CAMILLE exokernel for smart cards. We apply our technique to ensure trust between collaborative real-time extensions with the aim of supporting safe dynamic loading of scheduling policy.
ISSN:1206-212X
1925-7074
DOI:10.1080/1206212X.2005.11441752