Treffer: SecureChange public project deliverable D6.6: Development-time and on-device interplay

This document summarizes the work performed in Task 6.6 of Work Package 6 of the SecureChange project funded by the European Commission within the Seventh Framework Programme. The overall objective of Work Package 6 is the development of verification techniques for evolving systems, with a strong focus on the development time and deployment time phases of the software lifecycle. In the first two years of the project, WP6 developed several technologies to support verification of evolving systems. These technologies include off-device, development-time verification techniques, and on-device, deployment-time verification techniques. For the off-device techniques, the theory was developed in the first year (reported in deliverable D6.1), and a prototype was developed in the second year (reported in deliverable D6.2). In the third and final year, work has focused on the evaluation and validation of these results in the SecureChange case studies. This deliverable D6.6 reports on the application of our off-device verifier to the POPS and HOMES case studies. In summary, our results show that our prototype verifier is ready to handle real industrial code (both JavaCard and C code), that verification is performed fast even on code bases of thousands of lines of code, and that verification finds bugs. On the downside, we find that applying our verification technique is labor intensive. In particular, we find that the annotation overhead (i.e. the amount of annotation that the developer/verification engineer has to provide) is relatively high. To counter this disadvantage, we have started to work on inference of annotations, and report on the first results in this direction. For the on-device techniques, the theory was developed in the first two years of the project (reported in deliverables D6.3 and D6.4), and a prototype implementation of the most promising techniques for JavaCard was developed in the third and final year, and is reported on in deliverable D6.5. The prototype deliverable D6.5 (released together with this ...