Work Package 5 : Case Studies
This work package will evaluate the different prototypes developed in
the pro ject on their ability to check the security requirements identified at the beginning of the pro ject. To assess the effectiveness of the tools, we will use real-world case studies taken from different application areas.
Most of the work performed in this work package will be done at a
later stage of the pro ject.Nevertheless the selection of relevant
case studies and the choice of the application areas will bedone at
the beginning of the pro ject, as soon as the different kinds of
properties to check have been identified and classified.
Scientific objectives
This work package has two ob jectives:
- To validate the usability of the security requirements selected in WP 1 on a representative
set of applications and their ability to cover the different application areas; and
- To evaluate the capacity of the tools developed in WP 2, WP 3
and WP 4 to check those requirements. A preliminary list of application areas has been established:
- Telecommunication, here at least two different subareas have been identified:
- Mobile phones: handsets support different Java J2ME
profiles (MIDP, Docomo I-mode or Mophun for example). Mobile STIP is
another J2ME profile for mobile devices targeted at critical security
sensitive applications (like banking applications). Each profile has
its own security model and its own set of rules to enforce a coherent
security policy.
- Home gateways, and more specifically set-top-boxes using MHP, a standard defined for
services using digital television, are a very promising application field.
- The Internet, where notably Grid computing and active networks
are interesting application areas, where strong security properties
should be checked on pieces of mobile code.
- Updates of libraries in Java profiles or in Java-based
operating systems (e.g. Savage on mobile phones).
The selection of relevant examples is an important phase of this work
package. Industrial members of the project can only provide case
studies related to their field and the technology they use (Java
profile). To ensure a complete coverage of the other application
areas, the End User Panel will be asked to contribute by supplying some other relevant examples.
Structure of the work package
To ensure that the evaluation process covers both the different
properties identified in WP 1 and the different technologies developed
within WP 2, 3 and 4, we have defined the following tasks.
- Task 5.1 Selection of Case Studies
- Selection of relevant examples by the industrial members of the consortium and members of the End User Panel.
- Task 5.2 Evaluation of Type-based Verification Techniques
- Evaluation of the tools developed in WP 2 for information flow control, alias control and resource control.
- Task 5.3 Evaluation of Logical Verification Techniques
- Evaluation of the program verification environment developed in WP 3. We will check the capacity to handle generic properties but also application specific security properties. The handling of concurrency, the level of modularity, and the extent to which type-based analysis can improve logical analysis will be evaluated.
- Task 5.4 Evaluation of the Proof Carrying Code Infrastructure
- Evaluation of the Proof Carrying Code infrastructure developed in WP 4. Both off-line checker and on-device checker will be analyzed with emphasis on relative coverage, speed and resource requirements (file size overhead, memory).