Commit 99035f3a authored by Stanley Clark's avatar Stanley Clark
Browse files

Updated README

parent 3afe8c69
......@@ -5,31 +5,29 @@ This is the project containing the prototype for a security-aware query processo
## Setup & Execution
We use [Docker](https://www.docker.com/) as a wrapper to uniformly handle the whole experiment pipeline for better reproducibility.
Other commands related to Docker are based on shell scripts and should be run on a LINUX environment e.g. WSL on Windows.
To start, install [Git](https://git-scm.com/), and Docker.
Run the following:
Then, run the following:
```shell
git clone git@gitlab.tue.nl:stanrogo/saqp/saqp-optimiser.git
cd saqp-optimiser
git submodule update --init
# Copy the environment files (and change defaults if needed):
cp experiments/.env.example experiments/.env
cp pg-cuckoo/PgCuckoo/config-blank.ini pg-cuckoo/PgCuckoo/config.ini
# Build and launch services
docker-compose up -d
# Next, let's set up the database for a scale factor 1 TPC-DS dataset:
docker-compose exec postgres ./gen_tpcds.sh 1
docker-compose exec postgres ./populate_db.sh tpcds1
docker-compose exec postgres /home/app/postgres/gen_tpcds.sh 1
docker-compose exec postgres /home/app/postgres/populate_db.sh tpcds1
# Now, let's build the Java project:
docker-compose run builder mvn initialize
docker-compose run builder mvn package
# Copy the environment files (and change defaults if needed):
cp experiments/.env.example experiments/.env
cp pg-cuckoo/PgCuckoo/config-blank.ini pg-cuckoo/PgCuckoo/config.ini
# Setup Haskell Stack dependencies for the first time
docker-compose run optimiser /bin/sh -c "cd /home/pg-cuckoo/PgCuckoo && stack install --allow-different-user"
......@@ -37,102 +35,34 @@ docker-compose run optimiser /bin/sh -c "cd /home/pg-cuckoo/PgCuckoo && stack in
docker-compose run optimiser
```
This will first build two images and start two respective containers: one containing a PostrgeSQL 10 database instance, and the other containing haskell, java and maven build dependencies.
Then, the PostgreSQL database is populated with the TPC-DS data generated during building, PgCuckoo is compiled, and finally the java container executes the experiments.
The results of the experiments are in the generated `experiments/app/results/results-<scale_factor>.csv` file.
The `postgres` container hosts a PostgreSQL 10 database with PgCuckoo extensions installed.
We also use this container also to generate the TPC-DS data and to populate the database.
The `builder` image allows us to build maven projects in a container.
Although there is a default directory for this image, this can be changed simply by specifying
a different volume location.
Finally, the `optimiser` image includes Java and Haskell dependencies required to run the package
generated by the `builder`.
To run a Maven project after making changes and having performed the initial setup, the following commands are enough:
```shell
docker-compose run builder mvn package
docker-compose run optimiser
```
To stop the docker containers running, you can use `docker-compose down` to completely remove the services, from your system.
Alternatively, use `docker-compose stop` and `docker-compose start` to stop and start the containers while leaving stored information intact.
## Development
There are a number of maven executions, using the `exec:java` goal, available:
- Run the main test pipeline: `mvn exec:java@TestPipeline`
- Run the planning tests: `mvn exec:java@TestPlanning`
- Run exhaustive enumeration: `mvn exec:java@TestExhaustive`
- Run xacml policy generation: `mvn exec:java@XacmlGen`
There are two ways of getting to a state where you can successfully run these commands.
### Docker
The docker tooling is for those who do not wish to go through the hassle of installing everything by themselves.
There is a nice guide for debugging using IntelliJ [here](https://blog.jetbrains.com/idea/2019/04/debug-your-java-applications-in-docker-using-intellij-idea/).
The default docker script runs the experiment suite, but using `docker run` you can probably run anything else you like.
You can use this variant for making small changes, and for publishing the application in a way that is easily reproducible for others.
After the initial build and population of PostgreSQL with TPC-DS data, the database will not re-populate itself.
If you wish to experiment yourself in more detail or run the tool in an external environment you should change both the `experiments/app/.env` and `experiments/pg-cukoo/PgCuckoo/config.ini` files to reflect the PostgreSQL database you want to target.
### Local
For an integrated development experience, many, many things need to be installed.
The way to install dependencies for this project vary based on the host system being used.
Nevertheless, the following set of instructions can be followed to some degree:
1) Install the following prerequisites:
1) [OpenJDK 14](https://openjdk.java.net/projects/jdk/14/) - latest LTS version of Java
2) [Maven](https://maven.apache.org/) (latest) - used for the build system to manage dependencies
3) [PostrgeSQL 10](https://www.postgresql.org/) - A database to query TPC-DS data (version 10 due to PgCuckoo dependency)
4) [Haskell Platform](https://www.haskell.org/platform/) - Tools required to build PgCuckoo PostgreSQL query plan generator
2) Clone the repo and initialise submodules
```bash
git clone git@gitlab.tue.nl:stanrogo/saqp/saqp-optimiser.git
cd saqp-optimiser
git submodule update --init
```
3) Install the prerequisites specified in the `postgres/tpc-ds` directory (WSL or Unix required)
4) Create the TPC-DS benchmark dataset and generate the required queries.
```bash
cd tpc-ds
make_tpc.bash -h=<psql_hostname> -p=<psql_port> -u=<psql_user> \
-ps=<psql_password> -qd=<output_query_dir> \
-sf=<scale_factor>
```
This will create a database called `tpcds` within the specified cluster.
5) Run `postgres/sql/make-subject-tables.sql` to add subject tables to the tpcds database.
6) Copy `experiments/app/.env.example` to `experiments/app/.env` and overwrite with the details of the tpcds database
7) Install the PgCuckoo PostgreSQL hook (WSL or Unix required):
```bash
cd postgres/pg-cuckoo/PgExtension
make && make install
psql -c "CREATE EXTENSION cuckoo"
```
8) Compile the PgCuckoo tooling for the first time:
```bash
cd experiments/pg-cuckoo/PgCuckoo
stack install
```
9) Copy the PgCuckoo DB config and overwrite with the details of the tpcds database
```bash
cd experiments/pg-cuckoo/PgCuckoo
cp config-blank.ini config.ini
```
10) Build the maven project using the `pom.xml` file
```bash
mvn clean
mvn initialize
mvn compile
```
## Structure
This repository contains two sub-directories:
A quick overview of the contents of each of the directories in this project:
- [experiments](experiments) - contains the Java and haskell code used to execute the experiments
- [analysis](analysis) - the R code for the analysis of the experimental results
- [builder](builder) - the Docker file for the Maven project builder container
- [comparison](comparison) - the scripts for the execution of queries on both IBM DB2 and Oracle DB
- [experiments](experiments) - the Java code for the SAQP optimiser
- [pg-cuckoo](pg-cuckoo) - a submodule of the pg-cuckoo repo, allowing to run PostgreSQL plans directly
- [policy-gen](policy-gen) - a Java generator for policies into the required formats by IBM DB2, Oracle DB and the SAQP Optimiser
- [postgres](postgres) - contains the PostgreSQL tooling to easily create a new instance of a TPC-DS populated database
- [queries](queries) - SPJR queries based on TPC-DS
- [query-plans](query-plans) - some query plans for the queries in [queries](queries)
- [tpc-ds](tpc-ds) - a submodule of the tpc-ds repo, allowing to generate TPC-DS benchmark data and queries
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
%!TEX root = ../paper.tex
%============================================================================%
\begin{table}[!t]
\centering
\small
\caption{Results of running $C \difference (C \semijoin O)$ on $\database$ and $\secd{\database}$.}
\label{tab:a_priori_not_sound}
\begin{subtable}[t]{0.5\columnwidth}
\centering
\caption{$\evalnormal{\database}{C \semijoin O}$}
\begin{tabular}{|c|c|}
\hline
customer\_id & region \\\hline
1 & EU \\\hline
\end{tabular}
\end{subtable}%
\begin{subtable}[t]{0.5\columnwidth}
\centering
\caption{$\evalnormal{\database}{ C \difference (C \semijoin O)}$}
\begin{tabular}{|c|c|}
\hline
customer\_id & region \\\hline
2 & US \\\hline
\end{tabular}
\end{subtable}%
\newline
\vspace*{1mm}
\newline
\begin{subtable}[t]{0.5\columnwidth}
\centering
\caption{$\evalnormal{\secd{\database}}{C \semijoin O}$}
\begin{tabular}{|c|c|}
\hline
customer\_id & region \\\hline
1 & NULL \\\hline
\end{tabular}
\end{subtable}%
\begin{subtable}[t]{0.5\columnwidth}
\centering
\caption{$\evalnormal{\secd{\database}}{ C \difference (C \semijoin O)}$}
\begin{tabular}{|c|c|}
\hline
customer\_id & region \\\hline
1 & NULL \\\hline
2 & US \\\hline
\end{tabular}
\end{subtable}
\end{table}
% $Id: fitch.sty,v 1.6 2003/06/28 16:53:00 johanw Exp $
% Macros for Fitch-style formal proofs
% Johan W. Klüwer, June 10, 2001
% EDITS (Alexander W. Kocurek, June 8, 2019)
% %\RequirePackage{mdwtab,latexsym,amsmath,amsfonts,ifthen}
% - too many fonts were loading
% - removed mdwtab, which redefines tabular, causing several conflicts such as overriding color in tabular cells and redefining \hline so that \hline without arguments no longer works
\RequirePackage{mathtools,amsmath,ifthen}
% Line height in proofs
\newlength{\fitchlineht}
\setlength{\fitchlineht}{1.5\baselineskip}
% Horizontal indent between proof levels
\newlength{\fitchindent}
\setlength{\fitchindent}{0.7em}
% Indent to comment
\newlength{\fitchcomind}
\setlength{\fitchcomind}{2em}
% Line number width
\newlength{\fitchnumwd}
\setlength{\fitchnumwd}{1em}
% Altered from mdwtab.sty: shorter vline, for start of subproof
\makeatletter
\newcommand\fvline[1][\arrayrulewidth]{\vrule\@height.5\fitchlineht\@width#1\relax}
\makeatother
% Ordinary vertical line
\newcommand{\fa}{\vline\hspace*{\fitchindent}}
% Vertical line, shorter: Use at start of (sub)proof
\newcommand{\fb}{\fvline\hspace*{\fitchindent}}
% Hypothesis
\newcommand{\fh}{\fvline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Hypothesis, with longer vert line: for >1 hypothesis
\newcommand{\fj}{\vline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
% Modal subproof: takes argument = operator
\newcommand{\fitchmodal}[1]{%
\makebox[0pt][r]{${}^{#1}$\,}\fvline\hspace*{\fitchindent}}
\newcommand{\fn}{\fitchmodal{\Box}}% Box subproof
\newcommand{\fp}{\fitchmodal{\Diamond}}% Diamond subproof
% Modal subproof with hypothesis in first line (as in Fitch)
\newcommand{\fitchmodalh}[1]{%
\makebox[0pt][r]{${}^{\footnotesize #1}$\,}%
\fvline%
\makebox[0pt][l]{{%
\raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}%
\hspace*{\fitchindent}}
\newcommand{\fm}{\fitchmodalh{\Box}}% Box subproof with hypothesis
\newcommand{\fq}{\fitchmodalh{\Diamond}}% Diamond subproof with hypothesis
% Rule: formula introduction marker. \fr with line, \fs without line
\newcommand{\fr}{%
\makebox[0pt][r]{${\rhd}$\,\,}\vline\hspace*{\fitchindent}}
\newcommand{\fs}{%
\makebox[0pt][r]{${\rhd}$\,\,}}
% Box around argument, like new variable in ql
\newcommand{\fw}[1]{\fbox{\footnotesize $#1$}}
%
\newcounter{fitchcounter}
\setcounter{fitchcounter}{0}
%To avoid starting from 1, \setboolean{resetfitchcounter}{false}
\newboolean{resetfitchcounter}
\setboolean{resetfitchcounter}{true}
%To avoid increasing numbers, \setboolean{increasefitchcounter}{false}
\newboolean{increasefitchcounter}
\setboolean{increasefitchcounter}{true}
%\formatfitchcounter can be altered if need be, though only once per proof
\newcommand{\formatfitchcounter}[1]{\scriptsize \arabic{#1}}
%Typeset the counter
\newcommand{\fitchcounter}{%
\ifthenelse{\boolean{increasefitchcounter}}{\addtocounter{fitchcounter}{1}}{}
\formatfitchcounter{fitchcounter}}
%A line with a special number -- a tag, e.g. \ftag{\vdots}{}
\newcommand{\ftag}[2]{\multicolumn{1}%
{!{\makebox[\fitchnumwd][r]{\footnotesize $#1$}\hspace{\fitchindent}}>{$}l<{$}@{\hspace{\fitchcomind}}}%
{#2}} % Arc put the tag in math mode by default
% Main environments
% Arc modified the next two environments by replacing Ml (which is supposed to force math mode, left aligned in mdwtab) with >{$}l<{$}, which has the same effect in tabular
\newenvironment{fitchnum}%
{\ifthenelse{\boolean{resetfitchcounter}}{\setcounter{fitchcounter}{0}}{}
\begin{tabular}{!{\makebox[\fitchnumwd][r]{\fitchcounter }\hspace{\fitchindent}}>{$}l<{$}@{\hspace{\fitchcomind}}l}}%
{\end{tabular}}
\newenvironment{fitchunum}%
{\begin{tabular}{!{\makebox[\fitchnumwd][r]{}\hspace{\fitchindent}}>{$}l<{$}@{\hspace{\fitchcomind}}l}}%
{\end{tabular}}
\newenvironment{fitch}{\renewcommand{\arraystretch}{1.5}
\begin{fitchnum}}{\end{fitchnum}}
\newenvironment{fitch*}{\renewcommand{\arraystretch}{1.5}
\begin{fitchunum}}{\end{fitchunum}}
% The following is useful for giving a numbered formula, then the proof.
\newenvironment{flem}[2]%
{\begin{eqnarray}
&#1\label{#2}\\
&\begin{fitch}}%
{\end{fitch}\notag\end{eqnarray}}
%To write comment field for two consecutive lines, with brace
\newcommand{\ftwocom}[1]{%
\parbox[t]{3cm}{
\raisebox{-.6\baselineskip}[\baselineskip][0pt]{%
$\left.
\begin{aligned}
\,\\ \,
\end{aligned}
\right\}$\quad #1}
}}
\ No newline at end of file
%!TEX root = ../paper.tex
%============================================================================%
\section{Future Work}
\label{appendix:future_work}
In this appendix, we list all proofs and theory related to exploring soundness, security and maximality under conditions other than incomplete databases and inference-based property definitions.
Under the approach which allows inference of data outside of that permitted by the policy, the following set of implication rules can be derived:
%
\begin{itemize}
\item Soundness: $\tone \in \evalnormal{\database}{\secq} \implies \ttwo \in \evalnormal{\database}{\query} \wedge \tone \subsumed \ttwo$
\item Security: $\tone \in \evalnormal{\database}{\secq} \implies \tone \in \maskeddbprojection$
\item Maximality: $\tone \in \maskeddbprojection \wedge \ttwo \in \evalnormal{\database}{\query} \wedge \tone \subsumed \ttwo \implies \tone \in \evalnormal{\database}{\secq}$
\end{itemize}
%
Soundness is the same as for the anti-inference definitions.
However, both approaches are now secure since a different set of tuples is permitted.
The next question is: is the new definition of security contained in the old definition, i.e.\ does $ \forall_{\done \in \equivalentD}[\tone \in \evalnormal{\done}{\secq}] \implies (\tone \in \evalnormal{\database}{\secq} \implies \tone \in \secd{\database})$ hold?
Given a database $\database$ we have $\tone \in \evalnormal{\database}{\secq}$ by for-all elimination.
Further, we know that $\secd{\database}$ must be in the set $\equivalentD$.
So we have $\tone \in \evalnormal{\secd{\database}}{\secq}$, which in turn means that $\tone \in \secd{\database}$.
It is interesting to see how the old and new definitions relate to each other.
Essentially, in the new definition, due to weaker security, maximality allows more tuples, even those that you could infer something from; therefore a-priori filters out too many tuples to begin with.
In the old definitions, the notion of security is that of non-inference, and therefore a-posteriori applies predicates too late, whereby we are able to infer contents of the database.
\begin{proposition}
A-priori, new, complete, incomplete $\rightarrow$ secure.
\end{proposition}
\begin{proof}
We prove that $\forall_{\database, \policy, \query, \tuple}[\tuple \in \evalnormal{\secd{\database}}{\query} \implies \tuple \in \maskeddbprojection]$.
Because $\evalnormal{\secd{\database}}{\query} \subseteq \maskeddbprojection$, this trivially holds.
Therefore, security holds.
\end{proof}
\begin{proposition}
A-priori, new, complete, incomplete $\rightarrow$ not maximal.
\end{proposition}
\begin{proof}
We prove by counterexample that $\exists_{\database, \policy, \query, \tone}[\tone \in \maskeddbprojection \wedge \ttwo \in \evalnormal{\database}{\query} \wedge \tone \subsumed \ttwo \implies \tone \not\in \evalnormal{\database}{\secq}]$.
Let $\schema = \{\,\rel\,\}$ with $\headerof{\rel} = \{\,\attname\,\}$, $\relinstance = \{\,\{\,(\attname, 0)\,\}\,\}$, $\database = \{\,\relinstance\,\}$, $\rowpolicy = \{\,(\rel, true)\,\}$, $\cellpolicy = \{\,(\rel.\attname, false)\,\}$, $\query = \sigma_{\rel.\attname = \rel.\attname}(\rel)$ and $\nameof{\relinstance} = \rel$.
%
Take the tuple $\tone = \{\,(\attname, \textnull)\,\} \in \maskeddbprojection$.
We know that $\{\,(\attname, 0)\,\} \in \evalnormal{\database}{\query}$ since a comparison of a non-\textnull{} value to itself is true.
Therefore we have $\tone \subsumed \ttwo$.
However, $\evalnormal{\secd{\database}}{\query} = \emptyset$ since $\textnull \neq \textnull$.
The tuple $\tone$ is therefore not in $\evalnormal{\secd{\database}}{\query}$ and so maximality does not hold.
\end{proof}
\begin{proposition}
A-priori, old, complete $\rightarrow$ not maximal.
\end{proposition}
\begin{proof}
% --- Non-tuple-based proof ---
% We prove by counterexample. Let $\schema = \{\,\rel\,\}$ with $\headerof{\rel} = \{\,\attname\,\}$, $\relinstance = \{\,\{\,(\attname, 0)\,\}\,\}$, $\database = \{\,\relinstance\,\}$, $\rowpolicy = \{\,(\rel, true)\,\}$, $\cellpolicy = \{\,(\rel.\attname, false)\,\}$, $\query = \sigma_{\rel.\attname = \rel.\attname}(\rel)$ and $\nameof{\relinstance} = \rel$.
% The desired output is $\evalnormal{\database}{\secq} = \{\{\,(\attname, \textnull)\,\}\}$, since a comparison of a value to itself does not allow us to distinguish between two database instances.
% We know that $d{\database} = \{\,\{\,\{\,(\attname, \textnull)\,\}\,\}\,\}$.
% The certain answer to the query is then $\{\,\{\,(\attname, \textnull)\,\}\,\}$ since for any valuation $v(\{\,(\attname, \textnull)\,\})$, it is evident that the chosen constant is equal to itself.
% However, we have $\evalnormal{\database}{\secq} = \emptyset$ since $\textnull \neq \textnull$.
% The certain answer is not subsumed by the answer given by the ordering, and so \propertythree\ does not hold.
% --- Tuple-based proof ---
We prove by counterexample that $\exists_{\database, \policy, \query, \tone}[\tone \in \maskeddbprojection \wedge \forall_{\done \in \equivalentD}[\ttwo \in \evalnormal{\done}{\query} \wedge \tone \subsumed \ttwo] \implies \tone \not\in \evalnormal{\database}{\secq}]$.
Let $\schema = \{\,\rel\,\}$ with $\headerof{\rel} = \{\,\attname\,\}$, $\relinstance = \{\,\{\,(\attname, 0)\,\}\,\}$, $\database = \{\,\relinstance\,\}$, $\rowpolicy = \{\,(\rel, true)\,\}$, $\cellpolicy = \{\,(\rel.\attname, false)\,\}$, $\query = \sigma_{\rel.\attname = \rel.\attname}(\rel)$ and $\nameof{\relinstance} = \rel$.
%
Take the tuple $\tone = \{\,(\attname, \textnull)\,\} \in \maskeddbprojection$.
For any database instance in $\equivalentD$, by replacing the value of $\attname$ with any other value, that value will be equal to itself.
However, we have $\evalnormal{\database}{\secq} = \emptyset$ since $\textnull \neq \textnull$.
The tuple $\tone$ is therefore not in $\evalnormal{\database}{\secq}$ and so maximality does not hold.
\end{proof}
\begin{proposition}
A-posteriori, new, complete, incomplete $\rightarrow$ secure.
\end{proposition}
\begin{proof}
$\tone \in \evalnormal{\database}{\relsec{\query}} \implies \tone \in \maskeddbprojection$.
There is a $\ttwo \in \evalnormal{\database}{\query}$.
From the definition of $\relsec{\query}$ we know that $\tone \subsumed \ttwo$.
We also know that $\ttwo \in \database$.
This means that for the combination of selection conditions in $\query$, $\eval{\condition}{\ttwo} = 1$.
We know that $\tuple \in \rione \wedge \tuple \in \ritwo \implies (\tuple \in \relsec{\rione} \iff \tuple \in \relsec{\ritwo})$.
From this we conclude that $\tone \in \secd{\database}$ and a-posteriori is secure.
\end{proof}
\begin{proposition}
A-posteriori, new, complete, incomplete $\rightarrow$ maximal.
\end{proposition}
\begin{proof}
We prove that a-posteriori is maximal by proving $\ttwo \in \evalnormal{\database}{\query} \wedge \tone \in \secd{\database} \wedge \tone \subsumed \ttwo \implies \tone \in \evalnormal{\database}{\relsec{\query}}$.
Once again, this is proved by taking $\tuple \in \rione \wedge \tuple \in \ritwo \implies (\tuple \in \relsec{\rione} \iff \tuple \in \relsec{\ritwo})$.
\end{proof}
\begin{table}
\centering
\caption{Properties of the orderings under SPJR/named algebra, (in)complete databases, and (non-)inference security}
\begin{tabular}{ccccccc}
order & algebra & type & I/C & sound & secure & maximal \\
\toprule
a-pos & SPJR & old & C & $\checkmark$ & $\times$ & $\times$ \\
a-priori & SPJR & old & C & $\checkmark$ & $\checkmark$ & $\times$ \\
\midrule
a-pos & SPJR & old & I & $\checkmark$ & $\times$ & $\checkmark$ \\
a-priori & SPJR & old & I & $\checkmark$ & $\checkmark$ & $\checkmark$ \\
\midrule
a-pos & SPJR & new & I/C & $\checkmark$ & $\checkmark$ & $\checkmark$ \\
a-priori & SPJR & new & I/C & $\checkmark$ & $\checkmark$ & $\times$ \\
\midrule
a-priori & named & o/n & C & $\times$ & $\checkmark$ & $\times$ \\
a-priori & named & new & I & $\times$ & $\checkmark$ & $\times$ \\
a-priori & named & old & I & $\times$ & $\checkmark$ & $\checkmark$ \\
\bottomrule
\end{tabular}
\end{table}
All this is only possible under the assumption that we operate under incomplete databases.
If one were to take away the possibility of \textnull{} values in the original database, then maximality behaves in a different way, as well as the containment of the new definitions within the old being questioned as well.
\paragraph{Complete Databases}
In case of a complete database, the old inference based definition of security (and with it maximality) can lead to unexpected results.
First, the tuple based definition of $\rmax$ which we saw earlier, is based on an incomplete database.
Therefore, to give the counter example, we assume a database instance where $|\equivalentD| = 1$.
In this way $\rmax$ is always $\evalnormal{\database}{\query}$.
Assume a database schema $\schema = \{\, \rel \,\}$, policy $\policy$ masking cells where $b = 0$, a database $\database$ with $\relinstance = \evalnormal{\database}{\rel} = \{\{\,(a, 0), (b, 0)\,\}\}$ and a query $\query = \selection_{a=b}(\rel)$.
Then, $\equivalentD = \{\,\relinstance\,\}$.
From this, we get $\rmax = \relinstance$, which does not contain a masked value even though the policy says that it should be masked.
This means that the new definition of security is not contained within the old one for complete databases.
It also means that maximality cannot be achieved over a complete database by either algorithm.
One can argue that we cannot infer anything about external database contents this way, so this is the desired outcome, but is this really intuitive?
We argue that this is not.\nztodoin{This may be given in the discussion. (see also below)}
%!TEX root = ../paper.tex
%============================================================================%
\begin{figure}[!t]
\centering
\small
\fbox{
\begin{minipage}[c]{\columnwidth-2\fboxsep-2\fboxrule}
\centering
\begin{tabbing}
\hspace*{0.3cm}\=\hspace*{0.3cm}\=\hspace*{0.3cm}\=\hspace*{0.3cm}\=\hspace*{0.3cm}\= \kill
(\textsf{employee.role} $=$ `clerk' $\wedge$ \textsf{action\_id} = `read',\\
\> \textsf{pov}(\\
\>\> (\textsf{object} $=$ `customer', 1)\\
\>\> (\textsf{object} $=$ `order',\\
\>\>\> \textsf{fa}( \\
\>\>\>\> ($\textsf{order.customer.region} = \textsf{employee.region}$, 1)\\
\>\>\>\> ($\textsf{order.amount} < 500$, 1)\\
\>\>\> )\\
\>\> )\\
\>\> \textsf{dov}(\\
\>\>\> (\textsf{object} $=$ `order.amount' $\wedge$ $\textsf{order.amount} > 100$), 0)\\
\>\>\>(\textsf{object} $=$ `customer.region' $\wedge$ $\textsf{customer.region} = \textsf{EU}$, 0)\\
\>\>\> 1\\
\>\> )\\
\>\> 0\\
\> )\\
)
\end{tabbing}
\end{minipage}
}\\
\bigskip
\fbox{
\begin{minipage}[c]{0.91\columnwidth}
\begin{flushleft}
\textsf{employee.role} $=$ `clerk'
$\wedge$ \textsf{action\_id} = `read'
$\wedge$ (
\textsf{object} $=$ `customer'
$\vee$
(
\textsf{object} $=$ `order'
$\wedge$
(
\textsf{order.customer.region} $=$ \textsf{employee.region}
$\vee$
(
$\neg$\,(\textsf{order.customer.region} $=$ \textsf{employee.region})
$\wedge$
\textsf{order.amount} $<$ 500
)
)
)
$\vee$ (
$\neg$\,(
(
\textsf{object} $=$ `customer.region'
$\wedge$
$\textsf{customer.region} = \text{`EU'}$
)
$\vee$
(
\textsf{object} $=$ `order.amount'
$\wedge$
$\neg\,(\textsf{order.amount} <= 100)$
)
)
)
)
\end{flushleft}
\end{minipage}
}
\caption{ABAC policy}
\label{fig:policy}
\end{figure}
%!TEX root = ../paper.tex
%============================================================================%
\begin{proof}[Proof of \ref{rw:sec_assoc}]
We prove that for any relation instance $\relinstance \in \relationinstanceset$, attribute name $ \attname \in \headerof{\relinstance}$, security formulas $\sczero$ and $\scone$, and tuple $\tuple$, it holds that $\relinstance.\attname \notin \attributesin{\scone} \implies (\tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance)) \iff \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)))$.
\begin{fitch}
\fa \relinstance \in \relationinstanceset,\ \attname \in \headerof{\relinstance},\ \sczero,\ \scone,\ \tuple\\
\fj \relinstance.\attname \notin \attributesin{\scone}\\
\fa \fh \tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance))\\
\fa \fa \fw{\ttwo \in \rowop_{\scone}(\relinstance)} : \forall_{(\anone, \attval) \in \ttwo}[\anone \neq \attname \implies \tuple[\anone] = \ttwo[\anone]] \wedge \tuple[\attname] = \cellmask{\ttwo}{\attname}{\sczero} & $\cellop$-Def (F) + $\exists^{*}$-Elim (3)\\
\fa \fa \ttwo \in \relinstance & \Cref{lemma:row_level_subset} (4)\\
\fa \fa \cellmask{\ttwo}{\attname}{\sczero} = \cellmask{\ttwo}{\attname}{\sczero} & ????? (4, 5)\\
\fa \fa \fw{\tfour \in \cellop_{\sczero, \attname}(\relinstance)} : \forall_{(\anone, \attval) \in \ttwo}[\anone \neq \attname \implies \ttwo[\anone] = \tfour[\anone]] \wedge \tfour[\attname] = \cellmask{\ttwo}{\attname}{\sczero} & $\cellop$-Def (R) + $\exists^{*}$-Elim (5)\\
\fa \fa \tuple[\attname] = \tfour[\attname] & (4, 6, 7)\\
\fa \fa \fh (\antwo, \vone) \in \ttwo : \antwo \neq \attname & \\
\fa \fa \fa \antwo \neq \attname \implies \tuple[\antwo] = \tfour[\antwo] & $\forall$-Elim (4, 7, 9)\\
\fa \fa \forall_{(\antwo, \vone) \in \ttwo}[\antwo \neq \attname \implies \tuple[\antwo] = \tfour[\antwo]] & $\forall$-Intro (9, 10))\\
\fa \fa \tuple = \tfour & (8, 11)\\
\fa \fa \tuple \in \cellop_{\sczero, \attname}(\relinstance) & (7, 12)\\
\fa \fa \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)) & \Cref{lemma:row_filter_equality} (3, 4, 13)\\
\fa \tuple \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance)) \implies \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance)) & $\implies$-Intro (3, 14)\\
\fa \fh \tuple \in \rowop_{\scone}(\cellop_{\sczero, \attname}(\relinstance))\\
\fa \fa \tuple \in \cellop_{\sczero, \attname}(\relinstance) & \Cref{lemma:row_level_subset} (16)\\
\fa \fa \fw{\ttwo \in \relinstance} : \forall_{(\anone, \attval) \in \ttwo}[\anone \neq \attname \implies \tuple[\anone] = \ttwo[\anone]] \wedge \tuple[\attname] = \cellmask{\ttwo}{\attname}{\sczero} & $\cellop$-Def (F) + $\exists^{*}$-Elim (17)\\
\fa \fa \ttwo \in \rowop_{\scone}(\relinstance) & ????? (2, 18) \\
\fa \fa \cellmask{\ttwo}{\attname}{\sczero} = \cellmask{\ttwo}{\attname}{\sczero} & ????? (18, 19) \\
\fa \fa \fw{\tfour \in \cellop_{\sczero, \attname}(\rowop_{\scone}(\relinstance))} : \forall_{(\anone, \attval) \in \ttwo}[\anone \neq \attname \implies \tfour[\anone] = \ttwo[\anone]] \wedge \tfour[\attname] = \cellmask{\ttwo}{\attname}{\sczero} & $\cellop$-Def (R) + $\exists^{*}$-Elim (19)\\