In this project, we are designing a comprehensive security architecture that uses language-based mechanisms to eliminate errors due to circumvention of type safety, be they intentional or erroneous, and that additionally uses security policy mechanisms to contain malicious behavior. This approach extends techniques previously applied to mobile code and is based on a combination of a) mechanically verifying the absence of such errors in any software before it is run, using code representations that can be checked for such errors or that rule out errors in the first place, and b) monitoring executing software for malicious activity.

Our prototype system consists of multiple layers, each of which is secured by the layer below it, the lowest of which can be provided in tamper-resistant hardware. Key to the solution is to provide a typed hardware abstraction layer (THAL) that enables the construction of a type-safe system “from the ground up”, all the way down to the tamper-proof hardware. Hence, our goal is to build a practical system about which we can make security guarantees from the hardware up, and not just “from the operating system up”.

While handheld, battery-powered devices such as personal digital assistants (PDA's) and web-enabled mobile phones are emerging as new access points to the world's digital infrastructure, their cost and short battery life are factors that are holding back their enormous potential. Worse yet, the cost of such devices might even widen the “digital divide”. This research addresses these cost and battery-life issues simultaneously, thereby getting one step closer to a vision of ubiquitous computing embracing all of society. The specific focus is the digital university campus with wireless Internet coverage.

In this setting, the aim is to increase the utility and battery-life and decrease the cost of handheld wireless computers by enabling the use of relatively simple hardware for the mobile devices. This research aims both at designing embedded hardware that better conserves resources, as well as creating a software layer that masks the limited computational prowess of a handheld device by seamlessly coupling it to a relatively high-powered stationary computational infrastructure via an “always on” wireless connection. By off-loading power-intensive operations to the stationary infrastructure, the battery-powered mobile device is provided with “virtual power”.

We are developing adaptive just-in-time compiler technology for minimizing power use on mobile devices running mobile code, and adaptive scheduling methods using results from the Computational Grid research community. Depending on the algorithm to be run on the mobile device and its current distance from the nearest base station, the computation to be performed is automatically partitioned between a part to be executed in the stationary infrastructure and another to be run on the mobile device.

At the hardware level, we are developing orchestrated resource-management strategies to enable designers to correctly design and implement highly resource-constrained embedded systems while helping them to meet system-level constraints. This requires augmenting today's functional design flows with a resource-centric view. Here, the goal is not to replace existing design methodologies with yet another all-encompassing methodology, but rather making a cross-cutting impact by demonstrating the applicability of results to several driving examples at different levels of abstraction, including System-on-Chip (SoC) platforms, memory architecture level, and operating system level.

Given the acknowledged importance of existing and emerging mobile code technologies, remarkably little attention has so far been devoted to the management of mobile programs. The by far predominant model, which for example underlies the distribution of Java “applets” over the Internet, identifies dynamically linkable parts of mobile programs by a URL string. The model further assumes that the constituent parts that make up a mobile program will all be downloaded to a single location, and then verified, linked, possibly dynamically compiled, and finally executed at that very location.

It is immediately obvious that this model is far too primitive to capture the whole spectrum of meaningful distribution schemes for mobile code. There are many modes of mobile-code dissemination and deployment that are likely to be highly useful, but that are badly or not at all supported by current distribution models and architectures. What is needed is an overarching architecture that can describe not only current modes of mobile-code deployment, but also all meaningful future ones such as the physical separation of the machines performing verification, dynamic compilation, and execution, and support for the existence of multiple levels of security along the code distribution pipeline.

We are conducting methodical research to implement a prototype mobile-code distribution architecture. First, we are developing a comprehensive model that can capture all meaningful modes of mobile-code deployment, including issues of code versioning, code migration, and the differentiation between code validation, dynamic code translation between instruction formats, and code execution, which potentially could occur at multiple physically disjoint sites. This model provides a taxonomy of mobile-code distribution modes. Simultaneously, we are casting this model into an actual extensible distributed safe and secure code management architecture. As a practical application of this architecture, we are currently implementing a prototype system in which native code is generated at a firewall from a mobile-code distribution format and then downloaded to computationally restricted devices deployed in the theater via a secure high-bandwidth short-range wireless link

Second, our focus is on making a greater range of security policies amenable to automatic verification, by creating source-language constructs and accompanying type systems for representing these properties directly at the source-language level. Any such policy that can be cast into a language construct not only enables mechanical checking at the code receiver’s side, but also directly exposes these policies to the programmer rather than hiding them behind an API. It thereby raises the semantic level on which mobile code can be reasoned about and enhances the programmer’s understanding of the process.

Current mobile-code formats require verification by the code recipient to guard against potentially malicious actions of an incoming mobile program. Such verification is needed even when a mobile program originated in a “safe” language such as Java, because the transmission might have been corrupted by an adversary.

We have come up with an alternative approach based on a family of mobile code formats that simply don't allow illegal programs to be represented in the first place. In such an inherently safe format, any given bit-sequence of sufficient length is guaranteed to map back to a legal program in the original encoding domain, which in our prototype is Java. Hence, any incoming program that meets trivial well-formedness criteria is guaranteed to be legal and no code verification is necessary.

Our method enables the tamper-proof transport of performance enhancing annotations along with the program. In our current implementation, we are able to perform escape analysis at the code producer's side and can encode the results of this analysis in a manner that cannot be falsified in transit. Interestingly, adding annotations increases encoding density since it reduces the number of valid choices that need to be represented, so that the addition of the annotations comes at almost no space cost.

While our current implementation focuses on Java, the method is completely generic and can be adapted easily to other domains. To demonstrate this point, we were able to build an additional encoder for Oberon in less than a week.