Current Research

Verification of transformations on structured data

Tree and graph structured data, such as XML and RDF, are widely used in recent years. For transformations on such structured data, we study formalization of the following properties and how to verify formally whether the properties are satisfied or not.

(1) Information preservation
In data transformation, it is desirable that certain information in source data be preserved through transformation. However, there is a trade-off between conditionality of information preservation and flexibility of designs of transformations. Query preservation is known as one of formalizations for information preservation. Intuitively, query preservation means that any information obtained by the query to the source data can be extracted from the transformed data by some query. By specifying appropriate queries as parameters, query preservation can be a sensible condition for information preservation on transformations. The verification of query preservation is an important problem, but it is undecidable in general. In our research, we find for which classes of transformations on structured data query preservation is decidable, and formulate a verification method.

(2) Tolerance to inference attacks
For a database system to be secure, secrecy, integrity, and availability of data must be achieved appropriately with respect to a given security policy. View mechanisms have played a principal role in achieving the secrecy of database systems. Views (or transformations) can avoid direct accesses to sensitive information in the database. However, there still is a possibility of indirect accesses, i.e., the sensitive information can be inferred using authorized views and/or general domain knowledge. To measure such risk, metrics for safety against inference attacks is needed. Currently, we adopt k-secrecy as the metrics. The underlying concept of k-secrecy is that it can be considered to be insecure that the set of candidates for the value of the sensitive information can be narrowed down by inference. We are studying methods that checks whether data (and views) satisfy k-secrecy or not.