Mobile Resource Guarantees

These certificates will be condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgeable (proof-carrying code). Arbitrarily complex methods may be used by the code producer to construct these certificates, but their verification by the code consumer will always be a simple computation. One may compare this to the verification of alleged solutions to combinatorial problems such as Rubik's cube or the travelling salesman problem.

One way that a code producer may produce proofs of resource bounds is by using a programming language equipped with a linear resource-aware type system, whereby programs are certified by virtue of their typing as satisfying certain resource bounds. A corresponding proof at the bytecode level can be generated automatically from a typing derivation in such a system in the course of compiling the program to bytecode.

Scenarios of application for the proposed framework include the following.

• A provider of distributed computational power may only be willing to offer this service upon receiving dependable guarantees about the required resource consumption.
• A user of a handheld device, wearable computer, or smart card might want to know that a downloaded application will definitely run within the limited amount of memory available.
• Third-party software updates for mobile phones, household appliances, or car electronics should come with a guarantee not to set system parameters beyond manufacturer-specified safe limits.
• Requiring certificates of specified resource consumption will also help to prevent mobile agents from performing denial of service attacks using bona fide host environments as a portal.

Contact: