WG211/M10Bruneau

Formalized generation of programming frameworks by Julien Bruneau

Recently, platforms running third-party applications have become very
popular, in particular due to the explosion of the smartphone market.
One characteristic of these open platforms is to provide shared
resources to the applications that can either be hardware (camera,
GPS...), software (email client, web browser...), or data (user profile,
address book...). As third-party applications may have access to all
these shared resources, it is critical for the platform provider to
ensure that these applications behave safely.

The goal of our project is to ensure that these applications are safe.
To this end, our approach proposes a formalized generation of dedicated
programming frameworks. By formalizing our generator, we prove that
any application based on our development approach is conform to its
design. In particular, communication integrity is verified. Based on
this formalization, we ensure that domain-specific properties checked
at design-time (e.g., sensitive-data confinement) are correctly
propagated at compile-time and execution-time.