A-COMPASS: Formal Foundations for Anonymity Analysis in Microdata Tamara Tagliavia1 , Silvia Ghilezan1,2 1
Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade, Serbia 2 Faculty of Technical Sciences, University of Novi Sad, Novi Sad, Serbia
arXiv:2606.20492v1 [cs.CR] 18 Jun 2026
E-mail:
1
2
Abstract In the information age, one of the leading problems is how to ensure individual’s privacy. Depending on the context in which privacy is considered, various data privacy models have emerged. However, the domain of formal verification of these models is still not sufficiently explored even when it comes to the most basic models. An attempt to verify privacy requirements is the Compliance Assertion Language (COMPASS). In COMPASS, one can specify an anonymity condition that a table needs to satisfy, and an action that will modify the table if the condition is not satisfied. It is designed to operate on preprocessed tables in a form one record - one group of people. In this paper, we modify the COMPASS language in order to operate on microdata tables in their usual form of one record - one person. The modified language is called A-COMPASS. Along with checking of previously applied anonymity conditions, A-COMPASS enables the execution of anonymization actions as a new feature. We further provide the syntax and the semantics for the A-COMPASS language. We also prove the most important properties of the introduced semantics like determinism and compositionality. Finally, we provide a mechanism to verify anonymity properties, such as k-anonymity and l-diversity. Keywords A-COMPASS language, denotational semantics, privacy, anonymity,k-anonymity, l-diversity
1
Introduction
On a daily basis, a huge volume of data is collected from a variety of devices and platforms. Such data captures human behaviors, routines, activities, etc. Although the ability to manipulate large amount of data has improved our lives in many domains, it has also evolved new problems. The most important among them is certainly the data privacy problem. The first definition of privacy was given by Warren and Brandeis in 1890. in their “The Right to Privacy” [24], long before the information age. They define privacy as the right to be left alone. Nowadays, privacy is considered a fundamental right. Countries around the world have realized the need to protect the privacy of their citizens. The most important data protection legislation enacted to date is the General Data Protection Regulation (GDPR) [8]. The GDPR is a law originating from the EU, yet it applies to businesses all over the world that collect and process personal information of EU citizens. Such businesses are required to publish and abide a privacy policy agreement. A privacy policy is a statement that details how personal data provided by users will be collected, stored, processed, and shared with third parties. They are usually written in natural language, and thus their formal verification is very demanding. In parallel with the development of technology and the legal aspect of privacy, technologies for privacy protection also began to develop. In the core of these technologies are mathematical models and formal methods. One of the first models presented for data privacy is k-anonymity [22, 23], which deals with a special branch of privacy, called anonymity. It provides certain conditions that a microdata table has to fulfill in order to mitigate the risk of identity disclosure. A microdata record is considered to be a record that is associated with information of one individual. K-anonymity requires that one person in a microdata set cannot be distinguished from at least k-1 other persons with similar characteristics. The formal definition of k-anonymity is revisited
1
in Section 2. An improvement of this model is called l-diversity [17], and it deals with attribute disclosure, along with identity disclosure. When it comes to data privacy models, differential privacy [7], must be mentioned. Differential privacy deals mainly with privacy in aggregated statistics by adding noise to the query result. Therefore, it is a property of a mechanism (that adds noise), not a property of a table like the previous models. The research on mathematical models for privacy is increasingly developing, and there is an urge for formal verification of these models. Existing research on verification, such as [2, 9, 21], mainly deals with differential privacy, including sensitivity analysis over relational algebra [20]. In turn, basic models from the domain of anonymity still seek for more detailed formalization - a gap that formal methods in security suggest to be closed [4]. The basic anonymity models are widely used, and in order to be sure that certain privacy laws are adequately applied in practice, we need formal verification of these models. One of the pioneers in the verification of k-anonymity and l-diversity is a formal language called the Compliance Assertion Language (COMPASS) introduced in [10]. COMPASS is an SQL-based language designed to formulate anonymity requirements. Each COMPASS requirement is defined as an assertion followed by an action. An assertion represents the anonymity condition that the table has to satisfy, whereas the action represents the modification that has to be performed on the table if the assertion is not satisfied. The paper focuses on a special kind of tables that is preprocessed and in which each record represents a group of people. In a usual microdata table, each record represents one person. This limitation can be easily overcome by a slight extension of the COMPASS syntax. In this paper, we modify the syntax of COMPASS and we introduce it’s semantics.
Contributions The main contributions of the paper are: 1. We extend the COMPASS language into a new language called A-COMPASS (Anonymity Compliance Assertion Language) which can operate with tables in the form of one record - one person in addition to tables in the form one record - one group of people. This modification also allows the performance of anonymization actions(Section 3). 2. We modify the syntax of the COMPASS language by adding a new aggregation operation COUNT DISTINCT, removing the action JOIN, and extending the action ZERO into REPLACE(Section 3). 3. We provide a semantics for the A-COMPASS language(Section 4). 4. We prove fundamental properties of the introduced semantics, such as determinism and compositionality. We also validate anonymity properties of A-COMPASS using the introduced semantics(Section 5).
2
Anonymization in Microdata
A record that contains information related to a specific individual (a citizen or a company) is called microdata. The representation of microdata is usually in the form of a table, where each row represents a different individual, while each column contains information about the collected attributes. Therefore, a microdata table can be considered a special case of an SQL table. Table 1 is an example of a microdata table related to the annual electricity consumption. This kind of data is widely collected from surveys, administrative systems, or transactional processes and then forwarded to experts for analysis or published in the form of public statistics. There is a wide spectrum of applications of microdata, from medicine, economics, and social sciences to machine learning. However, microdata releases are very challenging for individual privacy [6]. Attribute Types. Attributes in microdata are classified into four categories: identifiers, quasi-identifiers, sensitive attributes, and non-sensitive attributes. An identifier uniquely identifies a person (e.g., social security number, a passport number). A quasi-identifier cannot uniquely identify a person; however, the combination of quasi-identifiers can lead to identification (e.g., name, age, profession, etc.). Sensitive attributes carry sensitive information about the individuals in the dataset (e.g., sex orientation, health condition, etc.). Non-sensitive attributes are those that don’t belong to any of the previous categories. Table 1 does not contain an identifier, since identifiers are the first to be removed when it comes to microdata publishing. Attributes Age and Postal Code are quasi-identifiers, whereas Annual Electricity Consumption (AEC) is the sensitive attribute.
2
Table 1: Non-anonymized microdata table
Table 2: Suppression method
Record ID
Age
Postal Code
AEC (kWh)
Record ID
Age
Postal Code
AEC (kWh)
1 2 3 4 5 6 7 8 9 10
54 54 54 82 86 83 36 36 45 45
21201 21201 21203 21410 21410 21410 21101 21102 21101 21102
2200 7400 8600 10500 3500 8600 4800 4800 6200 5400
1 2 3 4 5 6 7 8 9 10
54 54 54 80 80 80 36 36 45 45
21201 21201 21203 21410 21410 21410 21101 21102 21101 21102
2200 7400 8600 10500 3500 8600 4800 4800 6200 5400
Disclosure Risk. When it comes to anonymity and privacy issues in microdata releases, there are two associated disclosure risks: risk of an identity disclosure and risk of an attribute disclosure [13]. Identity disclosure occurs when an adversary links a record in the data with a specific individual. Then the values of the published attributes are also linked with that individual. Attribute disclosure occurs when an adversary can infer a value of a sensitive attribute for a specific individual with high probability. It can occur even without an identity disclosure. For example, if adversaries know that in the place with postal code 21410 lives only one person who is 86 years old (postal code 21410 represents a rural area), they can infer that the record with Record ID = 5 corresponds to that person. This is an example of an identity disclosure. Further, by looking at the value for AEC for this record, the adversary can conclude that this person lives alone (since 3500 kWh consumption per year does not represent high consumption). Moreover, if adversaries want to infer the AEC of a person who is 36 years old and lives in the town (the exact postal code is unknown, yet it is known that it is either 21101 or 21102), they cannot conclude which record belongs to that person (two records with Record ID = 7 and Record ID = 8 match). Thus, identity disclosure is not possible. However, since the value of AEC is the same for both records, they can learn its value with probability 1. Anonymization Methods. In order to mitigate disclosure risks, two base anonymization methods were introduced: suppression and generalization. Suppression is a method where certain values of the attributes are usually replaced by an asterisk, e.g., ’⋆’, [14, 22]. Replacing the attribute value with some other arbitrary value can also be considered a suppression method. Generalization is a method where all values of the attribute are replaced by a more general value [1, 15]. In this way, it can be considered that the values of that attribute are divided into categories. Example 1 (Suppression). Suppression is often used to cover rare values, since they represent a high risk for re-identification, e.g., ages over 80. When it comes to Table 1, if researchers conclude that for the data analysis an age category (not exact age) is enough, and if they want to protect the privacy of older individuals, they can decide to replace all values of an attribute Age that are over 80 with the value 80. Table 2 is an anonymized version of Table 1 obtained by the suppression method. Example 2 (Generalization). For statistical analysis, often knowing the area is sufficient, meaning that it is not necessary to know the exact town. That is why the values of the attribute Postal Code can be generalized by removing the last two digits. The new values of the attribute Postal Code now represent specific areas. Table 3 is an anonymized version of Table 1 obtained by the generalization method. The first data privacy models are based on these two anonymization methods. One of them is called kanonymity and it was introduced by Samarati and Sweeney in [22, 23]. The second one, called l-diversity, is essentially the extension of k-anonymity. It was introduced by Machanavajjhala et al. in [17] with the aim of improving the weaknesses of the previous model. Below we will recall the definitions of both models. Definition 1 (k-anonymity). Let R be a table with a set of attributes A. Let QR ⊆ A be a set of quasiidentifiers for table R. The table R satisfies the k-anonymity principle if and only if each combination of values of the attributes in QR is shared by k or more records. The k-anonymity principle says that an individual cannot be distinguished from at least k-1 other individu-
3
Table 4: 2-anonymity and 1-diversity
Table 3: Generalization method Record ID
Age
Postal Code
AEC (kWh)
Record ID
Age
Postal Code
AEC (kWh)
1 2 3 4 5 6 7 8 9 10
54 54 54 82 86 83 36 36 45 45
212** 212** 212** 214** 214** 214** 211** 211** 211** 211**
2200 7400 8600 10500 3500 8600 4800 4800 6200 5400
1 2 3 4 5 6 7 8 9 10
54 54 54 80 80 80 36 36 45 45
212** 212** 212** 214** 214** 214** 211** 211** 211** 211**
2200 7400 8600 10500 3500 8600 4800 4800 6200 5400
als that share the same combination of values of quasi-identifiers. The records of these individuals form an equivalence class. In this way k-anonymity provides protection against identity disclosure, up to some level k. However, k-anonymity is vulnerable to the homogeneity attack and the background knowledge attack. Both attacks refer to attribute disclosure. The homogeneity attack can be performed when all the values of the sensitive attribute in an equivalence class are the same. If an adversary concludes that someone’s data is in that equivalence class, they can exactly predict the sensitive value for that person. The background knowledge attack can be performed when the attacker uses some side (background) knowledge to reduce the set of possible values for the sensitive attribute. In order to overcome these attacks, the l-diversity model was developed [17]. Definition 2 (l-diversity). An equivalence class of a table R satisfies the l-diversity principle if and only if it contains at least l well-represented values for the sensitive attribute. The table R satisfies the l-diversity principle if and only if each equivalence class of R satisfies the l-diversity principle. Example 3 (k-anonymity and l-diversity). By applying both suppression and generalization methods from Example 4 and Example 5, Table 4 is obtained. This table has 4 equivalence classes. It satisfies the kanonymity principle for k=2, since the smallest equivalence classes have 2 records. It satisfies the l-diversity principle for l=1, since the values for the sensitive attribute in the third equivalence class are all the same. This class is also vulnerable to the homogeneity attack.
3
A-COMPASS Language
In order to verify whether a certain dataset satisfies anonymity requirements, the Compliance Assertion Language (COMPASS) was introduced in [10]. In COMPASS one can formulate the anonymity conditions that the dataset needs to satisfy and, if a condition is not satisfied, actions that need to be performed to modify the dataset to meet the defined anonymity criteria. We modify the COMPASS language in order to improve the anonymity analysis. Our goal is to extend the COMPASS language twofold: • to allow users to work with standard microdata tables in the form of one record - one person; • to allow users to anonymize a table by suppression and generalization.
3.1
A-COMPASS Syntax
The syntax of the A-COMPASS language is shown in Figure 1. We have introduced the commands in red. The rest of the commands are inherited from COMPASS language. In the following examples, we explain the A-COMPASS commands and how they are used to modify Table 1 and to perform anonymity analysis. Example 4 (Suppression in A-COMPASS). In order to obtain Table 2 from Table 1, the following A-COMPASS requirement needs to be applied.
4
EACH : :
RESULT Age ≤ 80 REPLACE Age WITH 8̇0;
The assertion EACH RESULT: Age ≤ 80 represents the condition we want our table to satisfy. The command EACH RESULT means that the assertion affects all records, Age ≤ 80 is the Boolean condition that has to be satisfied. If the assertion is not satisfied, action REPLACE Age WITH 80 replaces the values of the attribute Age with 80 in each record where Age > 80. NOTE: If the command SOME RESULT is used instead of EACH RESULT, only a subset of records is required to satisfy the defined condition, not necessarily all records. If the assertion is not satisfied in this case, action REPLACE Age WITH 80 will affect all records. requirements
::=
{ assertion ’:’ action ’;’ }
assertion
::=
( ’EACH’ result ’:’ boolExpr ) |( ’SOME’ result ’:’ boolExpr )
result resultQuery processQuery
::= ::= ::=
’RESULT’ |resultQuery processQuery |filterQuery ’PROCESS’ generalization [ ’WHERE’ boolExpr ] [ ’GROUP_BY’ attribute { ’,’ attribute } ]
generalization
::=
( ( ’SUM’ |’MIN’ |’MAX’ ) ’(’ attribute ’)’ ) |( ’COUNT’ ’(’ ’*’ ’)’ ) |( ’COUNT DISTINCT’ ’(’ ’attribute’) ) ’AS’ attribute
filterQuery
::=
’FILTER’ boolExpr
boolExpr boolProduct boolLiteral
::= ::= ::=
boolCond
::=
boolProduct { ’OR’ boolProduct } boolLiteral { ’AND’ boolLiteral } [ ’NOT’ ] boolCond |’(’ boolExpr ’)’ attribute ( ’<’ |’>’ |’=’ |’≤’ |’≥’ )( number |string )
action
::=
’REJECT’ |( ’REPLACE’ attribute ’WITH’ value ) |( ’RANDOM’ attribute lowerBound upperBound )
attribute value lowerBound upperBound
::= ::= ::= ::=
string string number number
Figure 1: The Syntax of the A-COMPASS language. Example 5 (Generalization in A-COMPASS). In order to obtain Table 3 from Table 1, the composition of the three following A-COMPASS requirements need to be applied. EACH : :
FILTER Postal code > ’21200’ AND Postal code < ’21299’ Postal code = ’212**’ REPLACE Postal code WITH ˙’212**’;
EACH : :
FILTER Postal code > ’21400’ AND Postal code < ’21499’ Postal code = ’214**’ REPLACE Postal code WITH ˙’214**’;
EACH : :
FILTER Postal code > ’21100’ AND Postal code < ’21199’ Postal code = ’211**’ REPLACE Postal code WITH ˙’211**’;
5
The assertions in all three requirements now represent accessing particular records, and the conditions that we want these particular records to satisfy. We explain the syntax on the example of the second requirement. In the second requirement, Postal code = ’214**’ represents the condition we want some records from our table to satisfy. The command EACH FILTER means that the assertion affects only filtered records that satisfy the Boolean expression Postal code > ’21400’ AND Postal code < ’21499’. If the assertion is not satisfied, action REPLACE Postal Code WITH ’214**’ replaces the value of the attribute Postal Code with ’214**’ only in the records where Postal Code starts with 214. NOTE: The same result can be achieved by the following A-COMPASS requirement. EACH : :
RESULT NOT (Postal code = ’21410’) REPLACE Postal code WITH ˙’214**’ ;
This approach gives the same result like the previous one since there is only one record in the table for which Postal code = ’21410’. However, the first approach is more intuitive because one filters the records that are to be affected and there is no need to handle the negation of a condition. Example 6 (OUTLIERS in A-COMPASS). Outliers can be very useful for statistical analysis, yet can also be misleading. Therefore, they require special attention from the perspective of statistical analysis. When it comes to anonymity analysis, they require even greater attention because they often contain highly revealing information. For example, the record with RECORD ID = 1 from Table 1 is an outlier record. In the case of identity disclosure, an adversary will associate a specific person with the value AEC=2200. The 2200 kWh for annual electricity consumption is too low even for one person living in a house, leading to the conclusion that very likely no one lives in this house. In order to preserve the privacy of the owner, the data curator might consider replacing the value AEC=2200 with some other value. Additionally, if the condition applies to multiple records in the table, the AEC value may be replaced in all of them. Let us assume that the minimum value corresponding to the consumption of one person is 3000 kWh, and that all values of AEC less than 3000 are too revealing. If we apply the deterministic approach, with the help of the REPLACE action, these values can be replaced, for example, with the mean value for AEC. The following A-COMPASS requirement represents this approach: EACH : :
RESULT AEC ≥ 3000 REPLACE AEC WITH 6̇200;
Replacing the outlier value with the mean value is the standard approach used in statistical analysis. However, it significantly changes the distribution of the attribute. That is why one can consider replacing the outlier value with some other value. For example, the data curator can decide to use the probabilistic approach and replace the values less than 3000 with a random value from the range that corresponds to the range of AEC values for household of one person. This approach does not affect the attribute distribution as much as the previous approach, and it is close to the differential privacy approach. The following A-COMPASS requirement represents the probabilistic approach: EACH : :
RESULT AEC ≥ 3000 RANDOM AEC 3000 4000;
The action RANDOM attribute lowerBound upperBound replaces the values of an attribute with an integer value between the lowerBound and the upperBound. It can also be used for categorical attributes, if preprocessing of the table is done in a way to replace the value of a category with an integer value. Example 7 (k-anonymity in A-COMPASS). The A-COMPASS assertion for Table 4 that corresponds to the k-anonymity condition is the following: EACH PROCESS :
COUNT(*) AS Class Size GROUP BY Age, Postal Code Class Size ≥ k;
This is an example of the A-COMPASS processQuery where COUNT(*) is used for generalization. This query counts the number of records in each group defined by Age and Postal Code. The counts represent the values of
6
a new attribute, Class Size. The Boolean condition Class Size ≥ k corresponds to the k-anonymity condition. Example 8 (l-diversity in A-COMPASS). The A-COMPASS assertion for Table 4 that corresponds to the l-diversity condition is the following: EACH PROCESS :
COUNT DISTINCT AEC AS Diversity AEC GROUP BY Age, Postal Code Diversity AEC ≥ l;
This is an example of the A-COMPASS processQuery where COUNT DISTINCT is used for generalization. This query counts the number of different values of the attribute AEC in each group defined by Age and Postal Code. The counts represent the values of a new attribute, Diversity AEC. The Boolean condition Diversity AEC ≥ l corresponds to the l-diversity condition. Example 9 (Homogeneity attack in A-COMPASS). As we have stated before, Table 4 is vulnerable to the homogeneity attack since all the values for the sensitive attribute in the third class are the same. This can be prevented by the action REJECT, which will delete all the records of the vulnerable equivalence class. EACH PROCESS : :
COUNT DISTINCT AEC AS Diversity AEC GROUP BY Age, Postal Code Diversity AEC > 1 REJECT;
Finally, by applying the previous A-COMPASS requirements to Table 1, Table 5 is obtained.
Table 5: Resulting table after ACOMPASS application
3.2
Record ID
Age
Postal Code
AEC (kWh)
1 2 3 4 5 6 9 10
54 54 54 80 80 80 45 45
212** 212** 212** 214** 214** 214** 211** 211**
3500 7400 8600 10500 3500 8600 6200 5400
A-COMPASS vs. COMPASS
In the following, we explain the main differences between the COMPASS and the A-COMPASS language. One Record - One Group vs. One Record - One Person. Standard microdata tables are in the form of one record - one person, like Table 1. However, COMPASS works only with pre-processed tables in the form of one record - one group. That means that the anonymization methods are already applied and a new attribute called Number is introduced. Number represents the number of persons in each group. COMPASS then allows reasoning about whether this pre-processed table satisfies some anonymity conditions. In addition to the tables in the form of one record - one group, A-COMPASS can also work with tables in the form of one record - one person. ZERO vs. REPLACE. The first modification of the syntax is in the generalization of the action ZERO from the COMPASS language into a new action REPLACE, which gives more flexibility. ZERO replaces the values of an attribute with the value 0, in turn, REPLACE allows the user to replace the values of an attribute with an arbitrary value. This action also enables the suppression of an attribute, e.g., Example 4. In addition, a composition of requirements with REPLACE enables the generalization of an attribute, e.g., Example 5. Furthermore, standard COMPASS language does not allow reasoning about l-diversity in the standard one record - one person setting. In order to do this in COMPASS, two steps are needed. First, duplicates must be collapsed, so each sensitive value appears only once per equivalence class. Then it can be counted how
7
many records exist per group. In order to do so, sub-queries are needed, or a composition of two requirements. However, sub-queries are not defined. The composition of two queries is also not possible because there is no action in COMPASS that can collapse duplicates. That is why we introduce COUNT DISTINCT, a new aggregation operation in A-COMPASS. COUNT DISTINCT. The second modification is in the extension of the COMPASS language with a new aggregation operation called COUNT DISTINCT, which counts the distinct values of an attribute. This aggregation operation allows reasoning about the l-diversity condition in the one record - one person setting, like in Example 8. No JOIN. The original COMPASS language supports JOIN action which allows users to join groups in one record - one group setting. Basically, the motivation behind the JOIN action is the generalization method. The action sums the values of the attribute Number for joined groups. In the A-COMPASS language, generalization can be performed by the composition of requirements with REPLACE action. That is why A-COMPASS does not contain (and need) the action JOIN. To summarize, from the aspect of syntax, requirements from Example 6 (RANDOM part) and Example 7, are examples of correct syntax in both COMPASS and A-COMPASS language, while requirements from Examples 4, 5, 6 (REPLACE part), 8, 9 are correct only in A-COMPASS. Looking at the broader picture, from the aspect of the table type to which these requirements apply, all presented examples are correct only in A-COMPASS.
3.3
A-COMPASS vs. SQL
Both A-COMPASS and COMPASS are SQL based languages. Consequently, they inherit a large part of SQL features. In the following, we elaborate the main similarities and differences between A-COMPASS and SQL that are relevant for the problem. Sets vs. Bags. The SQL semantics introduced in [12], is defined over bags (multisets). The A-COMPASS semantics follows this principle. Although the first works on formal semantics of SQL were using set semantics [18, 19], it turned out that this approach is not expressive enough. Bag semantics is needed for calculations with duplicates. In the original table duplicate records are not allowed (due to the uniqueness of the primary key); however, when it comes to calculations with COUNT and SUM duplicate values can appear. It is the same in A-COMPASS. In fact, duplicates are the core of the anonymity analysis. Each record represents one person, while two identical records (if the primary key is not observed) represent two different persons with the same characteristics. The k-anonymity principle is based on this fact. Multiple Tables. While SQL deals with multiple tables at a time, A-COMPASS is always interpreted on a single input table. That is why in A-COMPASS we do not have to deal with disambiguation of attributes with the same name across tables as in SQL. In A-COMPASS, attributes are elements of a set of attributes, and the only requirement is that there are no attributes with the same name. SELECT Queries. In SQL, SELECT...FROM...WHERE is the main query type. In A-COMPASS, there are no queries in this form. However, the semantics of requirements with the filterQuery is the same as semantics of the FROM...WHERE, which is a part of the SELECT...FROM... WHERE query restricted to one table. Subqueries. SQL allows subqueries, such as SELECT...FROM ( SELECT...FROM...). They can also produce attributes with the same name. A-COMPASS does not support subqueries. Three-valued Logic. SQL operates with three-valued logic, using three truth values: true (t), false (f ) and unknown (u). The unknown is also called NULL. First, SQL supports missing values, and they are treated as NULLs. Second, NULL can also appear in conditions of a query or in queries with aggregate operations, such as SUM, MIN, MAX, COUNT, and COUNT DISTINCT. This happens when there are no records that satisfy the condition. COUNT and COUNT DISTINCT on an empty bag produce 0, while SUM, MIN, and MAX produce NULL. A-COMPASS operates with two-valued logic under certain justified restrictions. A-COMPASS is interpreted only on a complete table, without missing values. Therefore, the table with missing values is supposed to be preprocessed before the analysis in A-COMPASS. This restriction comes naturally since the
8
released tables with microdata are usually complete. There is no point in releasing the incomplete record. When it comes to queries with aggregate operations, they can be defined on non-empty bags to avoid NULL values. Such results are not relevant for the anonymity analysis, so the language does not lose anything on it’s expressiveness by using two-valued logic. Randomness. Most SQL engines use a deterministic pseudo-random number generator. Randomness is exposed through functions such as random() or RAND() whose range is [0, 1). However, formal semantics of SQL that explicitly model these functions are rarely addressed in the literature. The denotational semantics of programming languages in [3, 5] provide a purely deterministic semantics for probabilistic programs, using deterministic pseudo-random samplers, called deterministic stream or random trace. A-COMPASS semantics follows the same idea.
4
Semantics
In this section we develop the denotational semantics for the A-COMPASS language. Our approach is inspired by Guagliardo and Libkin [12], who introduce denotational semantics for SQL. First, we explain the data model and the notation we are going to use. Then we present the semantics.
4.1
Data Model and Notation
A-COMPASS data model takes into account two sets: • N - a countably infinite set of attribute names (Names), and • D - a non-empty set (without NULL) of values that populate the data-base(Domain) . The non-empty tuple of distinct names from N is called a schema. The domain set D comprises primitive domains, such as integers and strings. We assume that there is a well-defined semantics of predicates of base types. A record r is a tuple of elements from D. A relation R is a finite bag (multiset) of records 1 . With S = (A1 , A2 , · · · , An ) we denote the schema of the relation R, and with r = (a1 , a2 , · · · , an ) a record on the schema S. For the multiplicity of a record r in a bag R, we will use the following notation: • #(r, R) for the multiplicity of r in R; • r ∈k R for #(r, R) = k; • r ∈ R to indicate that r ∈k R for some k > 0; X • |R| = #(r, R) for the number of records in R (the cardinality of R). r
We will also use the following definitions of bag operations [11, 16]: • #(r, R1 ∪ R2 ) = #(r, R1 ) + #(r, R2 ); • #(r, R1 ∩ R2 ) = min(#(r, R1 ), #(r, R2 )); • #(r, R1 − R2 ) = max(#(r, R1 ) − #(r, R2 ), 0). For turning a bag into a set (which will be needed for COUNT DISTINCT) we are going to use duplicate elimination operation ε defined in [12] in the following way: #(r, ε(R)) = min(#(r, R), 1). For actions REPLACE and RANDOM, we need to define record update. 1
Bags will be denoted by curly braces unless explicitly stated otherwise.
9
Definition 3 (Record Update). For a record r = (a1 , a2 , · · · , an ) on a schema l(R) = (A1 , A2 , · · · , An ), an attribute Ai ∈ l(R) and a value a ∈ D, the update of the record is defined by r[Ai → − a] = (a1 , a2 , · · · , ai−1 , a, ai+1 , · · · , an ). For action RANDOM, we also need to define a random trace. Definition 4 (Random Trace). A random trace ρ is an infinite sequence ρ = (ρ1 , ρ2 , · · · ) ∈ [0, 1)N . A fixed random trace in the beginning (at the initial state) allows us to model RANDOM deterministically. For fixed ρ ∈ [0, 1) and integer bounds l (lowerbound) and u (upperbound), RANDOM returns the integer value random(l, u, ρ) = l + ⌊ρ · (u − l + 1)⌋. Therefore, the semantic state will be the pair (R, ρ), where R is a relation and ρ is a random trace. In order to obtain the semantics that is fully deterministic, we also need to define canonical ordering of a bag. Definition 5 (Canonical Ordering). For a bag R, the canonical ordering order(R) = (r1 , · · · , rm ) is a list of records in non-decreasing order, where each record appears as many times as it’s multiplicity in R. For the non-decreasing order, we assume the natural order for numbers and the lexicographic order for strings. Why do we need canonical ordering? The action RANDOM takes a record, takes one value from the random trace, and updates the record as described above. For the next record, it takes the next value from the random trace. However, bags do not have an order. When it comes to the semantics, different orderings of the same bag R will lead to different outputs (R, ρ) and the semantics will not be deterministic. This is why, at the beginning, we need to fix a random trace and the canonical ordering of the bag.
4.2
Semantics
Our goal is to design a semantics of the requirements of the A-COMPASS language. The semantics of a requirement r will be denoted by JrK. This is a function that takes as input: a relation R(a database) and a random trace ρ. The output of the function will be the relation and the random trace obtained by executing the requirement JrK(R, ρ). The schema of JrK(R, ρ) will be denoted by l(R). It represents the tuple of attribute names associated with JrK(R, ρ) and it is related to the first part of the requirement, the assertion. The schema is defined in Figure 2, depending on the type of the assertion.
l(R) = S, tuple of attribute names for the original relation l(RESULT) = l(R) l(FILTER φ) = l(R) l(PROCESS f (B) as C WHERE ψ GROUP BY (G1 , · · · , Gm )) = (G1 , · · · , Gm , C) l(PROCESS f (B) as C WHERE ψ) = (C)
Figure 2: The schema of the A-COMPASS requirements Now, we define a function that maps attribute names to values of a record. Definition 6 (Environment.). An environment is partial mapping from N , attribute names, to D, values. Given a schema S = (A1 , A2 , · · · , An ) and a record r = (a1 , a2 , · · · , an ) on S, the environment is defined by ηS,r (Ai ) = ai . In the following, we describe the semantics of the A-COMPASS language. The input of the semantic function J·K depends on the syntactic category in the matter: for terms, the only input is the environment; for predicates and assertions, the inputs are the relation and the environment; finally, for actions, the inputs are the relation,
10
environment, random trace and the affected bag 2 . Terms. A term is either a constant c from D, or an attribute reference A 3 . The semantics of a term(and tuple of terms) is given by the environment η in Figure 3.
JtKη =
PREDICATES ( true if JAKη θ JcKη = η(A) θ c holds JA θ cKη = false otherwise
TERMS ( η(A) if t=A c
if t=c
JN OT φKη = ¬JφKη
J(t1 , t2 , · · · , tn )Kη = (Jt1 Kη , Jt2 Kη , · · · , Jtn Kη )
Jφ1 AN D φ2 Kη = Jφ1 Kη ∧ Jφ2 Kη Jφ1 OR φ2 Kη = Jφ1 Kη ∨ Jφ2 Kη
Figure 3: Semantics of the A-COMPASS terms and predicates Predicates. Predicates correspond to A-COMPASS Boolean conditions(boolCond), Boolean literals(boolLiteral), Boolean products(boolProduct), and Boolean expressions(boolExpr). Their evaluation is two-valued JP Kη ∈ {true, f alse}. We distinguish the following cases:
• boolCond Boolean conditions are atomic predicates in a form A θ c, where A is an attribute reference, θ ∈ {<, >, =, ≤, ≥} is a comparison operator, c is a constant; • boolLiteral Boolean literal is a negation of a Boolean condition; • boolProduct and boolExpr Boolean product and Boolean expression represent the conjuction and the disjunction of Boolean conditions, respectively.
The semantics of A-COMPASS predicates is given in Figure 3.
4.2.1
Assertions.
The syntax of the A-COMPASS assertion is given by: assertion
::=
( ’EACH’ result ’:’ boolExpr ) |( ’SOME’ result ’:’ boolExpr )
In order to define the semantics of an assertion, we first need to define the semantics of a result. Result. The semantics of a result is given in Figure 4. It represents the whole relation (if the result is the keyword RESULT), or the semantics of a resultQuery (in all other cases). Further, we need the semantics of resultQuery. Since resultQuery is defined by either a filterQuery or a processQuery, we will first give the semantics of a filterQuery. filterQuery. The semantics of a filter query is defined in Figure 5. It corresponds to the FROM... WHERE part of the SELECT... FROM... WHERE query from SQL, and it represents the sub-bag of R composed of records that meet the defined condition. The multiplicity of a record in the sub-bag is the same as the 2
An affected bag by an assertion is not a syntactic category of the A-COMPASS language. However, it is a product of the assertion needed to perform an action. 3 We use the same notation for attribute names and attribute references. As an attribute name, A denotes an attribute (column) name in a schema S. As an attribute reference, A denotes the value of the attribute named A.
11
(
JresultK(R) =
R if result = ’RESULT’ JresultQueryK(R) otherwise
Figure 4: Semantics of the A-COMPASS result multiplicity of the same record in R.
JFILTER φK =
r, . . . , r r ∈k R, JφKη = true
| {z } k times
Figure 5: Semantics of the A-COMPASS filter query For the aggregation in processQuery, we will use the following definition of aggregate functions on bags. Definition 7 (Aggregate Functions). For a bag R on a schema S and an attribute A ∈ S, summation, maximization, minimization, counting, and distinct counting are defined by: • SU MA (R) =
P
r∈R #(r, R) · JAKηS,r ;
• M AXA (R) = max{JAKηS,r , r ∈ R}; • M INA (R) = min{JAKηS,r , r ∈ R}; • COU N T∗ (R) = |R|;
• COU N T DIST IN CTA (R) = |ε({JAKηS,r , r ∈ R})|. processQuery. Let PROCESS fB AS C [WHERE ψ][GROUP BY G] be a process query where f is an aggregate function applied to the attribute B (or *), C is the name of the introduced attribute, ψ is a Boolean expression used for filtering, G = (G1 , · · · , Gm ) where Gi ∈ S is a set of attributes from a schema S used for grouping. We will introduce the semantics of this query in three steps. 1. FILTERING. If WHERE ψ is present, the query first filters some records and produces a sub-bag of R. The filtered bag R′ is given by R′ = r, . . . , r r ∈k R, JψKηS,r = true . | {z } k times
If there is no filtering, R′ = R. 2. GROUPING. If GROUP BY G is present, the query then partitions the records of the filtered bag into groups. Each group will have it’s own group key. Let K denote a set of distinct group keys that occur in R′ . K is then given by: K = { JGKηS,r , r ∈ R′ }, where JGKηS,r = (JG1 KηS,r , · · · , JGm KηS,r ).
For a group with a group key g ∈ K, the sub-bag of records that constitutes this group is given by:
Gg =
r, . . . , r r ∈k R′ , JGKηS,r = g . | {z } k times
12
3. AGGREGATION. In the third step, the aggregate values per group fB (Gg ) are computed. If the grouping step is skipped, only one aggregate value f (R′ ) is computed for the entire filtered bag. The function f can be one of the aggregate functions we have defined above (applied to the attribute B and the corresponding sub-bag). Finally, the semantics of a processQuery is defined in Figure 6.
JPROCESS fB ASCWHEREψGROUP BY GK = {(g, fB (Gg )), g ∈ K} JPROCESS fB AS C WHERE ψK = {(f (R′ ))}
Figure 6: Semantics of the A-COMPASS process query When grouping is present, the multiplicity of each tuple (g, fB (Gg )) is one, since the group key is unique per group. If there is no grouping, there is only one tuple (f (R′ )). Finally, we define the semantics of an assertion. Let P = JresultK(R) with schema S ′ = l(result) (the result schema is precisely defined in Figure 2). The semantics of an assertion is then defined in Figure 7.
JEACH result φK(R) = true ⇐⇒ ∀r ∈ P : JφKηS′ ,r = true JSOME result φK(R) = true ⇐⇒ ∃r ∈ P : JφKηS′ ,r = true
Figure 7: Semantics of the A-COMPASS assertion 4.2.2
Affected Bag.
For each assertion there will be a bag of records which violates the assertion and needs to be altered by the following action. This bag will be called an affected bag and it is a sub-bag of the original relation R. If there are no records that violate the assertion, the affected bag will be an empty bag. For an assertion of the type ’SOME’ result ’:’ boolExpr, the affected bag will be the whole relation R. When an assertion with ’SOME’ is violated, it means that there are no records in the whole relation that satisfy the required condition. For an assertion of the type ’EACH’ result ’:’ boolExpr, we need to differentiate between several sub-types of assertions in order to define the affected bag. Definition 8 (Affected Bag for EACH RESULT : boolExpr). For a relation R and an assertion EACH RESULT : φ, where φ is a Boolean expression, the affected bag is defined by:
AFF(R, EACH RESULT : φ) = r, . . . , r r ∈k R, JφKηS,r = f alse . | {z } k times
Definition 9 (Affected Bag for EACH FILTER boolExpr : boolExpr). For a relation R and an assertion EACH FILTER ψ : φ, where ψ and φ are Boolean expressions, the affected bag is defined by:
13
AFF(R, EACH FILTER ψ : φ) =
r, . . . , r r ∈k R, JψKηS,r = true ∧ JφKηS,r = f alse . | {z } k times
Definition 10 (Affected Bag for EACH PROCESS with GROUP BY ). For a relation R and an assertion EACH PROCESS fB AS C WHERE ψ GROUP BY G : φ, where f is an aggregate function applied to the attribute B, C is the name of the introduced attribute, G = (G1 , · · · , Gm ) is a set of attributes from a schema S used for grouping, ψ and φ are Boolean expressions:
AFF(R, EACH PROCESS fB AS C WHERE ψ GROUP BY G : φ) =
r, . . . , r r ∈k R′ , JGKηS,r ∈ Kv , | {z } k times
where [Kv = {g ∈ K | JφKηS′ ,ra = f alse} and S ′ = (G1 , · · · , Gm , C) , ra = (g, fB (Gg)). Thus, for the affected bag of an assertion EACH PROCESS with FILTER and GROUP BY, we first need to identify a set of violating group keys Kv . The assertion condition φ is evaluated on a schema of the PROCESS query S ′ and an aggregated record ra from the semantics of the PROCESS query. To be more specific, we identify groups whose aggregate values do not meet the condition. Then, we identify records from the filtered bag R′ that constitute these groups. Definition 11 (Affected Bag for EACH PROCESS without GROUP BY). For a relation R and an assertion EACH PROCESS fB AS C WHERE ψ : φ, where f is an aggregate function applied to the attribute B, C is the name of the introduced attribute, and φ is a Boolean expression: • IF JPROCESS fB AS C WHERE ψKR ̸= ∅ and JφKηS′ ,ra = f alse, AFF(R, EACH PROCESS fB AS C WHERE ψ : φ) = R′ ; • Otherwise, AFF(R, EACH PROCESS fB AS C WHERE ψ : φ) = ∅. Here, S ′ = (C) is a schema of the PROCESS query without GROUP BY, and ra = (fB (R′ )) is a single aggregated record from the semantics of the PROCESS query.
4.2.3
Actions.
An action is executed if an assertion is violated. Actions transform the semantic state (R, ρ) in the way described below. REJECT action. The action REJECT removes all affected records from the table. If V is the affected bag for the required assertion, the semantics of the REJECT action is then given in Figure 8.
JREJECTK(R, ρ, V ) = (R − V, ρ) Figure 8: Semantics of the action REJECT We have already stated that for an assertion with SOME, the affected bag will be the whole relation V = R. In that case, the REJECT action will delete the entire table and JREJECTK(R, ρ, v) = (∅, ρ). REPLACE action. The action REPLACE A WITH a replaces the values of an attribute A with the value a in all affected records. Let V be the affected bag for the required assertion, the semantics of the action REPLACE A WITH a action is then given in Figure 9. RANDOM action. The action RANDOM A l u replaces the values of an attribute A with the random integer value between the lower bound (l) and the upper bound (u) in all affected records. Let V , |V | = m be the
14
JREPLACE A WITH a K(R, ρ, V ) = ((R − V ) ∪ Va , ρ) where
Va =
r[A − → a], . . . , r[A → − a] r ∈k V
|
{z
k times
}
Figure 9: Semantics of the action REPLACE affected bag and order(V ) = (r1 , · · · , rm ) be it’s canonical ordering. Since |V | = m the first m values of the random trace ρ will be consumed (one per record ri from the affected bag), and that is why we will decompose ρ in prefm (ρ) = (ρ1 , · · · , ρm ) and tailm (ρ) = (ρm+1 , ρm+2 , · · · ). The semantics of the action RANDOM is then given in Figure 10.
JRANDOM A l u K(R, ρ, V ) = ((R − V ) ∪ Vr , tailm (ρ)) where Vr = {ri [A 7→ random(l, u, ri )] | 1 ≤ i ≤ m}
Figure 10: Semantics of the action RANDOM 4.2.4
Requirements.
Finally, A-COMPASS requirement r is in the form assertion : action. Let V be the affected bag for the required assertion, the semantics for a requirement is then given in Figure 11.
(
JrK(R, ρ) =
(R, ρ) JactionK(R, ρ, V )
if JassertionK = true otherwise
Figure 11: Semantics of the A-COMPASS requirement
5
Properties of the Semantics
In this section, we prove the fundamental properties of the introduced semantics. We then validate the anononymity properties of A-COMPASS language using this semantics.
5.1
Fundamental Properties
Here we prove the determinism and the compositionality of the given semantics. Since we modeled RANDOM deterministically, it is essential to show that the output of the semantic function is uniquely determined for every requirement and every initial semantic state.
15
Theorem 1 (Determinism). For every requirement r and every semantic state (R, ρ) ∈ Σ, where Σ is a set of semantic states, there exists a unique state (R′ , ρ′ ) ∈ Σ such that JrK(R, ρ) = (R′ , ρ′ ). Proof. The semantics of A-COMPASS requirement is defined by: ( (R, ρ) if JassertionK = true . JrK(R, ρ) = JactionK(R, ρ, V ) otherwise That is why we have to distinguish between two cases: JassertionK = true and JassertionK = false: • JassertionK = true, then JrK(R, ρ) = (R, ρ) is uniquely determined; • JassertionK = false, then JrK(R, ρ) = JactionK(R, ρ, V ).
By the definition of an affected bag, V is uniquely determined for a fixed assertion. Moreover, if: - action = REJECT, then JREJECTK(R, ρ, V ) = (R − V, ρ) is uniquely determined; - action = REPLACE A WITH a, then JREPLACE A WITH aK(R, ρ, V ) = ((R − V ) ∪ Va , ρ) is uniquely determined, because of the definition of Va ; - action = RANDOM A l u, then JRANDOM A l uK(R, ρ, V ) = ((R − V ) ∪ Vr , tailm (ρ)) is uniquely determined, because of the canonical ordering of R and V and the decomposition of ρ = (prefm (ρ), tailm (ρ)), which are fixed. Therefore, JrK(R, ρ) is uniquely determined in all cases.
Since A-COMPASS program is defined by sequential composition, it is essential to show what is the output of that program. Theorem 2 (Sequential composition). Let r1 , r2 , · · · , rn be a non-empty finite sequence of A-COMPASS requirements. Then ∀(R, ρ) ∈ Σ, where Σ is a set of semantic states, it holds: Jr1 ; r2 ; · · · ; rn K(R, ρ) = (Jrn K ◦ Jrn−1 K ◦ · · · ◦ Jr1 K) (R, ρ). Proof. We prove the statement by the induction on sequence length n. • Base case (n=1) Jr1 K(R, ρ) = Jr1 K(R, ρ) holds for all (R, ρ) ∈ Σ.
• Induction hypothesis (n=k) Asssume that for some k > 1, it holds Jr1 ; r2 ; · · · ; rk K(R, ρ) = (Jrk K ◦ Jrk−1 K ◦ · · · ◦ Jr1 K) (R, ρ). • Induction step (n=k+1) Let Pk+1 = r1 ; r2 ; · · · ; rk+1 and Pk = r1 ; r2 ; · · · ; rk , which is of the length n. Then Pk+1 = Pk ; rk+1 and JPk+1 K(R, ρ) = JPk ; rk+1 K(R, ρ) = (Jrk+1 K ◦ JPk K) (R, ρ). By the induction hypothesis: JPk+1 K(R, ρ) = Jrk+1 K ◦ (Jrk K ◦ · · · ◦ Jr1 K) (R, ρ). By the asociativity of function composition, it follows JPk+1 K(R, ρ) = (Jrk+1 K ◦ Jrk K ◦ · · · ◦ Jr1 K) (R, ρ).
16
5.2
Anonymity Properties
Here we validate the following anonymity properties of A-COMPASS language: suppression soundness, generalization soundness, RANDOM soundness with respect to outlier treatment, k-anonymity soundness and completeness, and l-diversity soundness and completeness. First we give definitions of anonymity properties expressed in A-COMPASS semantics. Definition 12 (Indistinguishability). Two records r1 , r2 ∈ R are indistinguishable with respect to A ∈ S, where S = l(R), if r1 ∼A,R r2 ⇐⇒ JAKηS,r1 = JAKηS,r2 . Indistinguishability among records can also be defined with respect to multiple attributes (S ′ ⊆ S) in a similar way: r1 ∼S ′ ,R r2 ⇐⇒ JS ′ KηS,r1 = JS ′ KηS,r2 .
Definition 13 (Equivalence Class). Let QI = (Q1 , Q2 , · · · , Qm ) ⊂ S be a tuple of quasi-identifiers for a relation R. The equivalence class of a record r ∈ R with respect to QI is the sub-bag of R defined by
[r]QI,R =
r, . . . , r r ∈k R, r ∼QI,R r . | {z } k times
Definition 14 (k-anonymity by A-COMPASS semantics). Let QI = (Q1 , Q2 , · · · , Qm ) ⊂ S be a tuple of quasi-identifiers for a relation R. The relation R satisfies the k-anonymity principle if and only if ∀r ∈ R, |[r]QI,R | ≥ k. Definition 15 (l-diversity by A-COMPASS semantics). Let QI = (Q1 , Q2 , · · · , Qm ) ⊂ S be a tuple of quasiidentifiers for a relation R. Let A ⊂ S be the sensitive attribute for the same relation. The relation R satisfies the l-diversity principle if and only if ∀r ∈ R, |ε({JAKηS,r , r ∈ [r]QI,R })| ≥ l. Theorem 3 (Suppression soundness). For any R, let JREPLACE A WITH aK(R, ρ, V ) = (R′ , ρ) where R′ = (R − V ) ∪ Va , V is the affected bag for a certain assertion, while Va is the corresponding replacing bag for the action REPLACE A WITH a. Then ∀r1 , r2 ∈ V, r1′ , r2′ ∈ [r]A=a,R′ where r1′ and r2′ are the transformed records of r1 and r2 respectively, and [r]A=a,R′ is the equivalence class in R′ that corresponds to A = a. Proof. Let us choose two arbitrary records from the affected bag, r1 , r2 ∈ V . By the semantics of the action REPLACE A WITH a, r1′ , r2′ ∈ Va and JAKηS,r′ = a, JAKηS,r′ = a. 1
2
Since a = JAKηS,r′ = JAKηS,r′ ⇐⇒ r1′ ∼A,R′ r2′ 1
2
meaning that r1′ and r2′ are indistinguishable with respect to A. Finally, by the definition of an equivalence class r1′ , r2′ ∈ [r]A=a,R′ .
17
Interpretation of Theorem 3. Action REPLACE A WITH a groups all affected records into one equivalence class with respect to the attribute A, and thus enables suppression. As a result, REPLACE is sound with respect to suppression. Theorem 4 (Replace action enforces indistinguishability). For any R, let JREPLACE A WITH aK(R, ρ, V ) = (R′ , ρ), where R′ = (R − V ) ∪ Va , V is the affected bag for a certain assertion, while Va is the corresponding replacing bag for the action REPLACE A WITH a. Let [r]A=a,R and [r]A=a,R′ be equivalence classes that corresponds to A = a in R and R′ respectively. Then |[r]A=a,R′ | ≥ |[r]A=a,R |. Proof. Since R′ = (R − V ) ∪ Va , we have
|[r]A=a,R′ | = |[r]A=a,R−V | + |[r]A=a,Va | = |[r]A=a,R | − |[r]A=a,V | + |[r]A=a,Va |. From |Va | = |V | and [r]A=a,Va = Va , we have |[r]A=a,Va | = |V |. Therefore, |[r]A=a,R′ | = |[r]A=a,R |−|[r]A=a,V |+|V |. Considering that [r]A=a,V is a sub-bag of V , |[r]A=a,V | ≤ |V | and |V | − |[r]A=a,V | ≥ 0, leading to |[r]A=a,R′ | ≥ |[r]A=a,R |.
Interpretation of Theorem 4. Suppression with action REPLACE A WITH a enforces indistinguishability among records. After this action, there are more records that are indistinguishable with respect to A (and value a) than it was before. Theorem 5 (Generalization soundness). Let Q ∈ S be a quasi-identifier for a relation R, and S be a schema for R. Let g1 , g2 , · · · , gn be a non-empty sequence of generalization requirements, where gi ::= EACH RECORD φi : REPLACE Q WITH qi and qi ∈ {q1 , q2 , · · · , qn } is a generalization value from D. Let R0 , R1 , · · · , Rn be a non-empty finite sequence of relation states defined by: R0 = R, (Ri , ρi ) = Jgi K(Ri−1 , ρi−1 ). Let V1 , V2 , · · · , Vn be a non-empty finite sequence of affected bags for requirements g1 , g2 , · · · , gn . Assume: i) Vi ⊆ Ri−1 for all i ∈ {1, 2, · · · , n}; ii) Vi = Vi0 for all i ∈ {1, 2, · · · , n}, where Vi0 is the affected bag for R = R0 ; iii) Vi ∩ Vj = ∅ for all i ̸= j; iv)
n [
Vi = R.
i=1
Then, ∀r ∈ Rn , it holds JQKηS,r ∈ {q1 , q2 , · · · , qn }. Proof. By iii) and iv) it follows that each record r ∈ R belongs to exactly one Vi , i ∈ {1, 2, · · · , n}, so it is affected by only one qeneralization requirement gi , i ∈ {1, 2, · · · , n}. We prove the statement by the induction on n. • Base case (n=1) We show that ∀r ∈ R1 , JQKηS,r ∈ {q1 }. By the definition of R1 and i) we have (R1 , ρ1 ) = Jg1 K(R0 , ρ0 ) and R1 = (R0 − V1 ) ∪ Vq1 , where Vq1 is the replacing bag of V1 . From iv) we have: V1 = R = R0 . Therefore, r ∈ V1 and JQKηS,r = q1 ∈ {q1 }. • Induction hypothesis (n=k) Assume that ∀r ∈ Rk , it holds JQKηS,r ∈ {q1 , q2 , · · · , qk }.
• Induction step (n=k+1). We show that ∀r ∈ Rk+1 , JQKηS,r ∈ {q1 , q2 , · · · , qk+1 }. By the definition of Rk+1 and the Theorem 2 of sequential composition, we have: (Rk+1 , ρk+1 ) = Jgk+1 K (Rk , ρk ) . From i) we have Vk+1 ⊆ Rk and Rk+1 = (Rk − Vk+1 ) ∪ Vqk+1 , where Vqk+1 is the replacing bag for Vk+1 . Let us choose an arbitrary r ∈ Rk+1 . Therefore, either r ∈ (Rk − Vk+1 ), or r ∈ Vqk+1 : - if r ∈ (Rk − Vk+1 ), then by the induction hypothesis JQKηS,r ∈ {q1 , q2 , · · · , qk } ⊂ {q1 , q2 , · · · , qk+1 }; - if r ∈ Vqk+1 , then JQKηS,r = qk+1 ∈ {q1 , q2 , · · · , qk+1 }.
18
Interpretation of Theorem 5. After n sequential generalization requirements in which every record is affected by only one requirement and all records are affected by some requirement, i.e., affected bags are disjoint and their union is the whole relation, values of the attribute Q will be replaced by a more general value in all records. There will be no record in which the value of Q will differ from one of the predetermined generalized values. Thus, composition of requirements with action REPLACE is sound with respect to generalization. Theorem 6 (RANDOM soundness w.r.t. outlier treatment). For any R, let JRANDOM A l uK(R, ρ, V ) = (R′ , ρ′ ), where R′ = (R − V ) ∪ Vr , V is the affected bag for a certain assertion, whereas Vr is the corresponding replacing bag for the action RANDOM. Then, ∀r ∈ V , JAKηR′ ,r′ ̸= JAKηR,r unless JAKηR,r ∈ [l, u] and random(l, u, ρ) = JAKηR,r . Proof. Let us choose an arbitrary record from the affected bag, r ∈ V . From the semantics of the action RANDOM A l u, JAKηR′ ,r′ = random(l, u, ρ) for some ρ ∈ [0, 1). We distinguish the following cases: • JAKηR,r ∈ / [l, u], then by the Definition 4 of random trace, random(l, u, ρ) = l + ⌊ρ · (u − l + 1)⌋, where ρ ∈ [0, 1), random(l, u, ρ) ∈ [l, u] for all ρ ∈ [0, 1), hence JAKηR′ ,r′ ̸= JAKηR,r ;
• JAKηR,r ∈ [l, u], then JAKηR′ ,r′ = JAKηR,r only if random(l, u, ρ) = JAKηR,r for some ρ ∈ [0, 1).
Interpretation of the Theorem 6. The point of the imputation method is to replace the outlier value with another value that reveals less information. Theorem 6 says that the replacing value JAKηR′ ,r′ will always be different from the original value of the outlier JAKηR,r , unless the original value is already in the interval [l, u] and random(l, u, ρ) is equal to the original value. However, for the proper treatment of outliers, the data curator will never choose the lower and the upper bound for the action RANDOM so that the original value belongs to [l, u], like in Example 6. As a result, RANDOM is sound with respect to outlier treatment. Theorem 7 (k-anonymity soundness and completeness). For any R, let JREJECTK(R, ρ, V ) = (R′ , ρ), where R′ = R − V and V is the affected bag for the assertion representing the k-anonymity condition. Then: i) R′ satisfies the k-anonymity principle. ii) For every S ⊆ R, if S satisfies the k-anonymity principle then S ⊆ R′ . Proof. Let QI = (Q1 , Q2 , · · · , Qm ) ⊂ S be a tuple of quasi-identifiers for a relation R and R′ . By the Definition 8 of an affected bag and by the Definition 14 of k-anonymity, we have V = r, . . . , r r ∈k R, |[r]QI,R | < k . | {z } k times
i) Let us choose an arbitrary r ∈ R′ and show that |[r]QI,R′ | ≥ k. Since r ∈ R′ and R′ = R − V , it holds r∈ / V and |[r]QI,R | ≥ k (1). Also, [r]QI,R = [r]QI,R′ (2). From (1) and (2), we have |[r]QI,R′ | ≥ k, which means that R′ satisfies the k-anonymity principle. ii) The proof is by contradiction. Let us choose S, an arbitrary sub-bag of R, which satisfies the k-anonymity principle, and S ⊈ R′ . Then, there exists a record r such that r ∈ S and r ∈ / R′ , meaning that r ∈ V and |[r]QI,R | < k. Since S ⊆ R, |[r]QI,S | ≤ |[r]QI,R | < k which is the contradiction with the assumption that S satisfies the k-anonymity principle. Therefore, S ⊆ R′ and |S| ≤ |R′ |.
Interpretation of the Theorem 7. The theorem says that the semantics of REJECT action is: i) sound with respect to k-anonymity, i.e., all remaining records satisfy the k-anonymity principle, and ii) complete with respect to k-anonymity, i.e., R′ is the largest obtainable sub-bag of R produced by REJECT. Theorem 8 (l-diversity soundness and completeness). For any R, let JREJECTK(R, ρ, V ) = (R′ , ρ) where R′ = R − V and V is the affected bag for the assertion representing the l-diversity condition. Then:
19
i) R′ satisfies the l-diversity principle. ii) For every S ⊆ R, if S satisfies the l-diversity principle then S ⊆ R′ . Proof. Let QI = (Q1 , Q2 , · · · , Qm ) ⊂ S be a tuple of quasi-identifiers for a relation R (and R′ ). Let A be the sensitive attribute for the same relations. By the Definition 8 of an affected bag and by the Definition 15 of l-diversity, we have V = r, . . . , r r ∈k R, |ε({JAKηS,r , r ∈ [r]QI,R })| < l . | {z } k times
i) Let us choose an arbitrary r ∈ R′ and show that |ε({JAKηS,r , r ∈ [r]QI,R′ })| ≥ l. Since r ∈ R′ and R′ = R − V , it holds r ∈ / V and |ε({JAKηS,r , r ∈ [r]QI,R })| ≥ l (1). Also, [r]QI,R = [r]QI,R′ (2). From (1) and (2), we have |ε({JAKηS,r , r ∈ [r]QI,R′ })| ≥ l, which means that R′ satisfies the l-diversity principle. ii) The proof is by contradiction. Let us choose S, an arbitrary sub-bag of R, which satisfies the l-diversity principle, and S ⊈ R′ . Then, there exists a record r such that r ∈ S and r ∈ / R′ , meaning that r ∈ V and |ε({JAKηS,r , r ∈ [r]QI,R })| < l. Since S ⊆ R, |ε({JAKηS,r , r ∈ [r]QI,S })| ≤ |ε({JAKηS,r , r ∈ [r]QI,R })| < l, which is the contradiction with the assumption that S satisfies the l-diversity principle. Therefore, S ⊆ R′ and |S| ≤ |R′ |.
Interpretation of the Theorem 8. The theorem says that the semantics of REJECT action is: i) sound with respect to l-diversity, i.e., all remaining records satisfy the l-diversity principle), and ii) complete with respect to l-diversity, i.e., R′ is the largest obtainable sub-bag of R produced by REJECT.
6
Discussion and Conclusion
We have extended the COMPASS language of [10], which is used for anonymity analysis in databases. The new language is called A-COMPASS. Beside the one record - one group setting in which COMPASS works, A-COMPASS can also work in one record - one person setting, which is more suitable for microdata analysis. Further, A-COMPASS enables users to perform anonymization methods, such as suppression and generalization, not only to check whether a certain anonymity conditions is applied. A-COMPASS extends the COMPASS syntax with an action REPLACE A with a, and a new aggregation operator COUNT DISTINCT, in order to allow reasoning about k-anonymity and l-diversity. We have exemplified A-COMPASS features on a microdata set related to annual electricity consumption. We have also introduced a semantics for A-COMPASS, inspired by SQL semantics of [12]. Finally, we have proven the determinism and compositionality of the introduced semantics, as well as soundness and completeness of the introduced actions with respect to anonymity analysis. Guagliardo and Libkin in [12] show the equivalence of their denotational semantics for SQL with relational algebra. Moreover, Palamidessi and Stronati in [20] investigate sensitivity bounds for differential privacy in relational algebra. Together, these two lines of research form a direction for future work. First, future work may investigate whether A-COMPASS requirements correspond to expressions in relational algebra. Second, in order to additionally allow privacy analysis, the extension of A-COMPASS may be considered. This approach also includes probabilistic RANDOM modeling so that the language can support working with concrete distributions and reasoning about differential privacy. Finally, the implementation of the language will be considered.
References [1] Gagan Aggarwal, Tomas Feder, Krishnaram Kenthapadi, Rajeev Motwani, Rina Panigrahy, Dilys Thomas, and An Zhu. k-anonymity: Algorithms and hardness. Technical report, Stanford University, 2004. [2] Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. Higher-order approximate relational refinement types for mechanism design and differential privacy. SIGPLAN Not., 50(1):55–68, January 2015. [3] Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda-calculus foundation for universal probabilistic programming. SIGPLAN Not., 51(9):33–46, September 2016.
20
[4] Michele Bugliesi, Stefano Calzavara, and Riccardo Focardi. Formal methods for web security. Journal of Logical and Algebraic Methods in Programming, 87:110–126, 2017. [5] Fredrik Dahlqvist, Alexandra Silva, and William Smith. Deterministic stream-sampling for probabilistic programming: semantics and verification. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1–13. IEEE, 2023. [6] Josep Domingo-Ferrer, David Sánchez, and Jordi Soria-Comas. Database Anonymization: Privacy Models, Data Utility, and Microaggregation-based Inter-model Connections, volume 8. 01 2016. [7] Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith. Calibrating noise to sensitivity in private data analysis. In Shai Halevi and Tal Rabin, editors, Theory of Cryptography, pages 265–284, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. [8] European Parliament and Council of the European Union. Regulations (EU) 2016/679 of the European Parliament and of the Council - general data protection regulation (GDPR), 2016. [9] Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear dependent types for differential privacy. SIGPLAN Not., 48(1):357–370, January 2013. [10] Richard Göbel and Stephanie Kitzing. Defining Anonymity Properties of Datasets with the Compliance Assertion Language (COMPASS). Digit. Gov.: Res. Pract., 4(3), September 2023. [11] Stéphane Grumbach and Tova Milo. 52(3):570–588, June 1996.
Towards Tractable Algebras for Bags.
J. Comput. Syst. Sci.,
[12] Paolo Guagliardo and Leonid Libkin. A formal semantics of SQL queries, its validation, and applications. Proc. VLDB Endow., 11(1):27–39, September 2017. [13] Anco Hundepool, Josep Domingo-Ferrer, Luisa Franconi, Sarah Giessing, Eric Schulte Nordholt, Keith Spicer, and Peter-Paul de Wolf. Statistical Disclosure Control. Wiley, 2012. [14] Roberto J. Bayardo Jr. and Rakesh Agrawal. Data privacy through optimal k-anonymization. In Karl Aberer, Michael J. Franklin, and Shojiro Nishio, editors, Proceedings of the 21st International Conference on Data Engineering, ICDE 2005, 5-8 April 2005, Tokyo, Japan, pages 217–228. IEEE Computer Society, 2005. [15] Kristen LeFevre, David J. DeWitt, and Raghu Ramakrishnan. Incognito: Efficient full-domain kanonymity. In Fatma Özcan, editor, Proceedings of the ACM SIGMOD International Conference on Management of Data, Baltimore, Maryland, USA, June 14-16, 2005, pages 49–60. ACM, 2005. [16] Leonid Libkin and Limsoon Wong. Query Languages for Bags and Aggregate Functions. Journal of Computer and System Sciences, 55(2):241–272, 1997. [17] Ashwin Machanavajjhala, Daniel Kifer, Johannes Gehrke, and Muthuramakrishnan Venkitasubramaniam. L-diversity: Privacy beyond k-anonymity. ACM Trans. Knowl. Discov. Data, 1(1):3, 2007. [18] J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Toward a verified relational database management system. In Manuel V. Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 237–248. ACM, 2010. [19] M. Negri, G. Pelagatti, and L. Sbattella. Formal semantics of SQL queries. ACM Trans. Database Syst., 16(3):513–534, September 1991. [20] Catuscia Palamidessi and Marco Stronati. Differential privacy for relational algebra: Improving the sensitivity bounds via constraint systems. In Herbert Wiklicky and Mieke Massink, editors, Proceedings 10th Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2012, Tallinn, Estonia, 31 March and 1 April 2012, EPTCS, pages 92–105, 2012. [21] Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP ’10, page 157–168, New York, NY, USA, 2010. Association for Computing Machinery. [22] Pierangela Samarati and Latanya Sweeney. Protecting privacy when disclosing information: k-anonymity and its enforcement through generalization and suppression. Technical report, CMU, SRI, 1998. [23] Latanya Sweeney. k-anonymity: A model for protecting privacy. Int. J. Uncertain. Fuzziness Knowl. Based Syst., 10(5):557–570, 2002. [24] Samuel D. Warren and Louis D. Brandeis. The right to privacy. Harvard Law Review, 4(5):193–220, 1890.
21