Logic-based information flow analysis approaches generally are high precision, but lack automatic ability in the sense that they demand user interactions and user-defined specifications. To overcome this obstacle, we propose an approach that combines the strength of two available logic-based tools based on the KeY theorem prover: the KEG tool that detects information flow leaks for Java programs and a specification generation tool utilizing abstract interpretation on program logic. As a case study, we take a simplified e-voting system and show that our approach can lighten the user’s workload considerably, while still keeping high precision.
CITATION STYLE
Do, Q. H., Kamburjan, E., & Wasser, N. (2016). Towards fully automatic logic-based information flow analysis: An electronic-voting case study. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9635, pp. 97–115). Springer Verlag. https://doi.org/10.1007/978-3-662-49635-0_6
Mendeley helps you to discover research relevant for your work.