http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM10BruneauWG211/M10Bruneau - Revision history2026-04-05T19:51:42ZRevision history for this page on the wikiMediaWiki 1.43.5http://mw.hh.se/wg211/index.php?title=WG211/M10Bruneau&diff=23&oldid=prevAdmin: 1 revision2011-12-12T10:06:23Z<p>1 revision</p>
<p><b>New page</b></p><div>[[Category:WG211]]<br />
<br />
<br />
<br />
'''Formalized generation of programming frameworks''' by Julien Bruneau<br />
<br />
Recently, platforms running third-party applications have become very<br />popular, in particular due to the explosion of the smartphone market.<br />One characteristic of these open platforms is to provide shared<br />resources to the applications that can either be hardware (camera,<br />GPS...), software (email client, web browser...), or data (user profile,<br />address book...). As third-party applications may have access to all<br />these shared resources, it is critical for the platform provider to<br />ensure that these applications behave safely.<br /><br />The goal of our project is to ensure that these applications are safe.<br />To this end, our approach proposes a formalized generation of dedicated<br />programming frameworks. By formalizing our generator, we prove that <br />any application based on our development approach is conform to its <br />design. In particular, communication integrity is verified. Based on <br />this formalization, we ensure that domain-specific properties checked <br />at design-time (e.g., sensitive-data confinement) are correctly <br />propagated at compile-time and execution-time.</div>Admin