Toward Security Verification against Inference Attacks on Data Trees
This work addresses security verification for data trees, but it is incremental as it builds on existing concepts to propose a decidable model.
The paper tackles the problem of verifying security against inference attacks on data trees by aiming to achieve infinite secrecy, where attackers cannot reduce sensitive information to a finite set of candidates. The result is a proposed model that makes infinite secrecy decidable through tree transducers and data tree types.
This paper describes our ongoing work on security verification against inference attacks on data trees. We focus on infinite secrecy against inference attacks, which means that attackers cannot narrow down the candidates for the value of the sensitive information to finite by available information to the attackers. Our purpose is to propose a model under which infinite secrecy is decidable. To be specific, we first propose tree transducers which are expressive enough to represent practical queries. Then, in order to represent attackers' knowledge, we propose data tree types such that type inference and inverse type inference on those tree transducers are possible with respect to data tree types, and infiniteness of data tree types is decidable.