Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning

M.-C. Jakobs, in: Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM), 2015, pp. 159--174.

Download
Restricted 250-Jakobs2015.pdf 724.31 KB
Conference Paper | English
Author
Abstract
Before execution, users should formally validate the correctness of software received from untrusted providers. To accelerate this validation, in the proof carrying code (PCC) paradigm the provider delivers the software together with a certificate, a formal proof of the software’s correctness. Thus, the user only checks if the attached certificate shows correctness of the delivered software.Recently, we introduced configurable program certification, a generic, PCC based framework supporting various software analyses and safety properties. Evaluation of our framework revealed that validation suffers from certificate reading. In this paper, we present two orthogonal approaches which improve certificate validation, both reducing the impact of certificate reading. The first approach reduces the certificate size, storing information only if it cannot easily be recomputed. The second approach partitions the certificate into independently checkable parts. The trick is to read parts of the certificate while already checking read parts. Our experiments show that validation highly benefits from our improvements.
Publishing Year
Proceedings Title
Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)
Page
159--174
LibreCat-ID

Cite this

Jakobs M-C. Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning. In: Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM). LNCS. ; 2015:159--174. doi:10.1007/978-3-319-22969-0_12
Jakobs, M.-C. (2015). Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning. In Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM) (pp. 159--174). https://doi.org/10.1007/978-3-319-22969-0_12
@inproceedings{Jakobs_2015, series={LNCS}, title={Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning}, DOI={10.1007/978-3-319-22969-0_12}, booktitle={Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)}, author={Jakobs, Marie-Christine}, year={2015}, pages={159--174}, collection={LNCS} }
Jakobs, Marie-Christine. “Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning.” In Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM), 159--174. LNCS, 2015. https://doi.org/10.1007/978-3-319-22969-0_12.
M.-C. Jakobs, “Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning,” in Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM), 2015, pp. 159--174.
Jakobs, Marie-Christine. “Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning.” Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM), 2015, pp. 159--174, doi:10.1007/978-3-319-22969-0_12.
Main File(s)
File Name
250-Jakobs2015.pdf 724.31 KB
Access Level
Restricted Closed Access
Last Uploaded
2018-03-21T09:45:15Z


Export

Marked Publications

Open Data LibreCat

Search this title in

Google Scholar