{'fraction_non_alphanumeric': 0.03812677861172594, 'fraction_numerical': 0.010367954201268119, 'mean_word_length': 4.506781524926686, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 1, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 9, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Blockaid: Data Access Policy Enforcement for Web Applications

Modern web applications serve large amounts of sensitive user data, access to which is typically governed by data-access policies. Enforcing such policies is crucial to preventing improper data access, and prior work has proposed many enforcement mechanisms. However, these prior methods either alter application semantics or require adopting a new programming model; the former can result in unexpected application behavior, while the latter cannot be used with existing web frameworks. Blockaid is an access-policy enforcement system that preserves application semantics and is compatible with existing web frameworks. It intercepts database queries from the application, attempts to verify that each query is policy-compliant, and blocks queries that are not. It verifies policy compliance using SMT solvers and generalizes and caches previous compliance decisions for better performance. We show that Blockaid supports existing web applications while requiring minimal code changes and adding only modest overheads.


Introduction
Many modern web applications use relational databases to store sensitive user data, access to which is governed by organizational or regulatory data-access policies. To enforce these policies, today's web developers wrap each database query within access checks that determine whether a user has access to the queried data. As an application can query the database at many call sites, getting access checks right at every call site is challenging, and erroneous or missing checks have exposed sensitive data in many production systems [4,32,39,40,48,66].
Prior work has suggested a variety of languages, frameworks, and tools that simplify the enforcement of data-access policies. As we detail in §2, these approaches either (1) require applications be written using specialized web frameworks, hindering their adoption; or (2) transparently remove from query results any data that cannot be revealed, possibly resulting in unexpected application behavior (e.g., the user has no idea that there are missing results and reaches the wrong conclusion).
This paper proposes an alternative approach to enforcing data-access policies that meets four goals: 1. Backwards compatibility: Applies to applications built using common existing web frameworks. 2. Semantic transparency: Fully answers queries that comply with the policy and blocks queries that do not (rather than providing partial, and potentially misleading, results). 3. Policy expressiveness: Supports a wide range of realistic data-access policies. 4. Low overhead: Has limited impact on page load time.
We implement this approach in a system called Blockaid, which enforces a data-access policy at run time by intercepting SQL queries issued by the application, verifying that they comply with the policy, and rejecting any non-compliant queries by raising an error. We assume that non-compliant queries are rare in production (having been mostly eliminated during testing), and focus on efficiently verifying compliant queries. Blockaid expects the developer to insert access checks as usual; it merely ensures that the checks are adequate.
A policy in Blockaid is specified using SQL view definitions defining what information that can be accessed by a given user, although the application still issues queries against the base tables as usual (rather than against the views). Under this setting, a query is compliant if and only if it never reveals-for any underlying dataset-more information than the views do, a wellstudied property in databases called query determinacy [52].
While determinacy does characterize the compliance of one query in isolation, it is too restrictive in the context of web applications, which typically issue multiple queries when serving a request. In this setting, what data is accessible often depends on the result of previous queries in the same web request. We thus extend determinacy to take a trace of previous queries and their responses, a novel generalization we call trace determinacy, and use that as the criterion for compliance.
To verify compliance, Blockaid frames trace determinacy as an SMT formula and checks it using SMT solvers. As we later explain, a solver returns an unsatisifiability proof when a query is compliant, and a test demonstrating a violation otherwise.
Unfortunately, this basic approach is impractically slow as SMT solvers are invoked for every query. Thus, we use a decision cache to record compliant query-trace pairs encountered so that future occurrences need not be rechecked. However, naively caching exact queries and traces would be ineffective since the exact queries appearing in a trace are specific to the user and page visited, and therefore a single query and trace are unlikely to be encountered multiple times.
Thus, to increase cache hit rate, we implement a novel generalization mechanism which, given a compliant query-trace pair, extracts a small set of assumptions on the query and trace that alone would guarantee compliance. These assumptions are cached in the form of a decision template, which will apply to all future query-trace pairs that meet those assumptions. Blockaid generates decision templates by progressively relaxing a query and trace while maintaining compliance, with the help of solver-generated unsatisfiable cores [8, § 11.8]. (It cannot cache non-compliance results because there is no unsat core. ) We applied Blockaid to three existing applicationsdiaspora* [27], Spree [65], and Autolab [5]-and found that it imposes an overhead of 2 % to 12 % to the median page load time when compliance decisions are cached.
Blockaid has some important limitations. It assumes that the application obtains all of its information through SQL queries visible to Blockaid or from a caching layer instrumented by Blockaid. It also only supports a subset of SQL and is at the mercy of solver performance and unsat-core size.

Related Work
The subject of data-access control has been studied by many. In this section, we compare Blockaid's approach to previous ones along our four design goals. Static verification. Several systems have been proposed to statically verify that application code can only issue compliant queries; examples include Swift [17], SELINKS [24], Ur-Flow [15], and STORM [44]. These systems incur no run-time overhead and can be more precise than Blockaid as they analyze source code. However, they typically require using a specialized language or framework like Jif [51] and Ur/Web [16], sacrificing compatibility with common web frameworks. Query modification. A popular run-time approach is query modification [67], where secret values returned by a query are replace by placeholders (or rows containing secret values are dropped). This is implemented in commercial databases [13,50] and in academic works including Jacqueline [74], Qapla [49], and Hippocratic databases [3]. While query modification allows programmers to safely issue queries without regard to policies, it lacks semantic transparency as it can alter query semantics in unexpected ways and return misleading results [34,60,71]. 1 Furthermore, query modification mechanisms typically use row-and cell-level policies (e.g., SQL Server RLS and DDM, Oracle VPD). As we discuss in §9, this row-/cell-level format 1 In general, correctly dealing with query modification requires solving the problem of query evaluation over incomplete information [21]. This problem has remained unresolved [23] for the last four decades.  Figure 1: An overview of Blockaid.
is less expressive than Blockaid's view-based scheme and cannot express many practical policies.
View-based access control. Many databases allow administrators to create views and grants access to views and tables. Although identical in expressiveness to Blockaid, this mechanism requires queries to explicitly use view names instead of table names (like Users). This marks a significant deviation regular web programming, as programmers must now sort out which views grant them information for each query. In contrast, Blockaid allows queries to be issued against the base tables directly. While prior work has studied view-based compliance of queries issued against base tables [10,11], they only check single queries, while Blockaid checks a query in the context of a trace, a crucial feature for supporting web applications.

Application Assumptions and Threat Model
Blockaid targets web applications that store data in and query data from a relational database using SQL. We assume that a user is logged in and that the current user's identifier is stored in a request context. The application can access the database and the request context when serving a request; each request is handled independently from others. We assume that the application authenticates the user correctly, and that the correct request context is passed to Blockaid ( §3.2).
A data-access policy dictates, for a given request context, what information in the database is accessible and what is inaccessible. We treat the database schema and the policy itself as public knowledge and assume that the user cannot use side channels to circumvent policies. We enforce policies on database reads only (as done in prior work [2, 10-12, 35, 43, 60, 63, 67, 71]). Ensuring the integrity of updates, while important, is orthogonal to our goal and is left to future work.

System Overview
Blockaid is a SQL proxy that sits between the application and the database (Figure 1). It takes as input (1) a database schema (including constraints), and (2) a data-access policy specified as database views ( §4), and checks query compliance for each web request separately. For each web request, it maintains a trace of queries issued so far and their results; the trace is cleared when the request ends. Blockaid assumes that results returned by queries in the trace are not altered till the end of the request.
At the start of a web request, the application sends the request context (including user ID) to Blockaid. Then, every SQL query from the application traverses Blockaid, which attempts to verify that the query is compliant, i.e., it only reveals accessible information. To do so, Blockaid consults the decision cache to see whether a similar query has been determined compliant before. If not, it encodes non-compliance as an SMT formula ( §5) and checks its satisfiability by invoking an ensemble of SMT solvers in parallel ( §7).
If a query is compliant, Blockaid forwards it to the database unmodified; in case of a cache miss, it also extracts and caches a decision template ( §6). Finally, it appends this query and its result to the trace. If verification fails, Blockaid blocks the query by raising an error to the application.
Although our core design assumes all sensitive information is stored in the relational database, Blockaid supports limited compliance checking for two other common data sources: 1. If the application stores database-derived data in a caching layer (e.g., Redis), the programmer can annotate a cache key pattern with SQL queries from which the value can be derived. Blockaid can then intercept each cache read and check the compliance of the queries associated with the key. 2. If the application stores sensitive data in the file system, it can generate hard-to-guess names for these files and store the file names in a database column protected by the policy. Blockaid's basic requirement is soundness: it must prevent the revelation of inaccessible information (formalized in §4.3). However, it may reject certain application behavior that does not violate the policy. We discuss ways to deal with such false positives in §9.
We end by emphasizing two aspects of Blockaid's operation: 1. Blockaid has no visibility into or control over the application (except by blocking queries). So it must assume that any data fetched by the application will be shown to the user. 2. Blockaid has no access to the database except by observing the results of application-issued queries. Thus, the application must only issue queries it knows to be compliant; it cannot expect Blockaid to ascertain its compliance by issuing additional queries.

Application Requirements
For use with Blockaid, an application must: 1. Send the request context to Blockaid at the start of a request and signal Blockaid to clear the trace at the end; 2. Handle rejected queries cleanly (although a web server's default behavior of returning HTTP 500 often suffices); and, 3. Not query data that it does not plan on revealing to the user.
Existing applications often violate the third requirement. For example, in the Spree e-commerce application, when a user requests to view a past order, it fetches the order from the database and only then, in application code, does it ensure the user is authorized to view the order. Such queries must be rewritten to fetch only data that is known to be accessible.

View-based Policy and Compliance
In this section, we explain how to specify a data-access policy using SQL views ( §4.1), how query compliance is defined for such a policy ( §4.2), and how it relates to Blockaid's overall goal of enforcing a policy on an application ( §4.3).
Throughout the paper, we will use as a running example a calendar application with the following database schema: Users(UId, Name) Events(EId, Title, Duration) Attendances(UId, EId, ConfirmedAt) where primary keys are underlined. The request context consists of a parameter MyUId denoting the UId of the current user.

Specifying Policies as Views
A policy is a collection of SQL queries that, together, define what information a user is allowed access. Each query is called a view definition and can refer to parameters from the request context. As an example, Listing 1 shows four view definitions, Notationally, for a view V and a request context ctx, we write V ctx to denote V with its parameters replaced with values in ctx. We often drop the superscript when the context is apparent.

Compliance to View-based Policy
Under a policy consisting of view definitions, Blockaid can allow an application query to go through only if it is certain that the query's result is uniquely determined by the views. In other words, an allowable query must be answerable using accessible information alone. If a query's output might depend on information outside the views-such information is by definition inaccessible-Blockaid must block the query. Looking at Listing 1, this query can always be answered using V 4 , which reveals the UId of everyone whom the user attends an event with, and V 1 , which supplies the names associated with these UId's. Hence, Blockaid allows it through.
This query above is allowed unconditionally because it is answerable using the views on any database instance. More commonly, queries are allowed conditionally based on what Blockaid has learned about the current database state from the trace of prior queries and results in the same web request. The application first queries the user's attendance record for Event #5-an unconditionally allowed query-and receives one row, indicating the user is an attendee. It then queries the title of said event. The user has access to this data because V 3 reveals the information on all events attended by the user. More precisely, the result of first query limits our scope to only database instances where the current user attends Event #5. Because the second query is answerable using V 3 on all such instances, it is conditionally allowed given the trace.
Context is important here: The second query cannot be safely allowed if it were were issued in isolation. Blockaid must block this query because it is not answerable using V on a database where the user does not attend Event #5.
Whether or not the user actually is an attendee of the event is irrelevant: The application, not having queried the user's attendance records, cannot be certain that the query is answerable using accessible information alone. This differs from alternative security definitions [34,41,75] where a policy enforcer can allow a query after inspecting additional information in the database that has not been fetched by the application.
where each Q i is a query and each O i is a collection of tuples.
Definition 4.5. Let ctx be a request context, V be a set of views, to V given T if for every pair of databases D 1 , D 2 that conform to the schema and database constraints, 2 and satisfy: we have Q(D 1 ) = Q(D 2 ). We will simply say compliant if the context is clear. Definition 4.5 extends the classic notion of query determinacy [52,62] with the trace; we thus name it trace determinacy. Query determinacy is undecidable even for conjunctive views and queries [29,30]; trace determinacy must also be undecidable for the same scenarios. Although several decidable cases have been discovered for determinacy [1,52,54], they are not expressive enough for our use case. A promising direction is to identify classes of views and queries that capture common web use cases and for which trace determinacy is decidable.

From Query Compliance to Noninterference
Blockaid's end goal is to ensure that an application's output only depends on accessible information. We now state this goal formally and then tie our query compliance definition to it.
We model a web request handler as a program P (ctx, req, D) that maps a request context ctx, an HTTP request req, and a database D to an HTTP response. 3 A program that abides by a policy V satisfies a noninterference property [22,31] stating that its output depends only on the inputs that the user has access to-namely, ctx, req, and V ctx (D) for each V ∈ V . Definition 4.6. A program P satisfies noninterference under policy V if the following condition holds: ).
An enforcement system must ensure that any program running under it satisfies noninterference. We now model such systems that operate under Blockaid's assumptions.
Definition 4.7. An enforcement predicate is a mapping from a request context, a query, and a trace to an allow/block decision: Definition 4.8. Let P (ctx, req, D) be a program and E be an enforcement predicate. We define the program P under enforcement using E as a new program P E (ctx, req, D) that simulates every step taken by the original program P , except that it maintains a trace T and blocks any query Q issued by P where E(ctx, Q, T ) = by immediately returning an error.
Note that P E invokes E only with traces in which every query has been previously allowed by E given its trace prefix. Definition 4.9. Given a request context ctx, we say that a trace Definition 4.10. A predicate E correctly enforces policy V if: We are ready to state the main result of this section, whose proof is left to Appendix A.
Theorem 4.11. Let V be a set of views and E be a predicate. Then for any request context ctx, query Q, and prefix E-allowed trace T such that E(ctx, Q, T ) = , Q must be ctx-compliant to V given T .
Theorem 4.11 illustrates two important properties of query compliance in relation to application noninterference: 1. Sufficiency: As long as only compliant queries from the application are let through, there is no way for an execution to be influenced by inaccessible information. 2. Necessity: Any enforcement system that makes per-query decisions based solely on the query and the trace cannot safely allow any non-compliant query without the risk of the application revealing inaccessible information. In this sense, we can think of query compliance as the "projection" of application noninterference onto the lens of Blockaid. This is why we adopt it as Blockaid's enforcement criterion.

Compliance Checking with SMT
To verify query compliance, Blockaid formulates (the negation of) query compliance as a logical formula ( §5.1), which it then discharges using SMT solvers. Our SMT formulation is based on the correspondence between relational algebra and first-order logic [20]; as a result, Blockaid must rewrite practical SQL queries into basic relational algebra, sometimes via approximation ( §5.2). Finally, it uses several optimizations to speed up compliance checking ( §5.3).

Translating Noncompliance to SMT
Blockaid translates query noncompliance (i.e, the negation of Definition 4.5) into an SMT formula; thus, a query is compliant if and only if the formula is unsatisfiable. We use a straightforward translation scheme based on Codd's theorem [20], which states, informally, that relational algebra under set semantics is equivalent in expressiveness to first-order logic (FOL). Relational algebra has five operators-projection, selection, cross product, union, and difference-and tables are interpreted as sets of rows (i.e., no duplicates). Under this equivalence, tables are translated to predicates in FOL, and operators can be implemented using existential quantifiers, conjunctions, disjunctions, and negations. Let E D (·, ·, ·) and A D (·, ·) be FOL predicates representing the Events and Attendances table in the database D in: Note that Q D is not a logical symbol, but merely a shorthand for the right-hand side.
Example 5.2. We now present the noncompliance formula for and Q D i encode the views and query on database D i (i = 1, 2) in FOL. The desired formula is the conjunction of: where x denotes a sequence of fresh variables. We can similarly encode database constraints and consistency with a trace.

Handling Practical SQL Queries
The encoding of relational algebra into logic, while straightforward, fails to cover real-world SQL due to two semantic gaps: 1. While the translation assumes that relational algebra is evaluated under set semantics, in practice databases use a mix of set, bag, and other semantics when evaluating queries. For example, a SQL SELECT clause can return duplicate rows, but the UNION operator removes duplicates. 2. SQL operations like aggregations and sorting have no corresponding operators in relational algebra. For Blockaid to bridge these gaps, it must first assume that database tables contain no duplicate rows. This is generally the case for web applications as object-relational mapping libraries like Active Record [61] and Django [28] add a primary key for every table. Given this assumption, Blockaid rewrites complex SQL into basic queries that map directly to relational algebra.

Basic SQL Queries
Definition 5.3. We call a query basic if it is a SELECT-FROM-WHERE query that never returns duplicate rows; or a UNION of SELECT clauses (which, by definition, removes duplicates). 4 A basic query on duplicate-free tables maps to relational algebra under set semantics, and so can be directly translated to FOL. To ensure a SELECT query is basic, we check it against these sufficient conditions for returning no duplicate rows: • It contains the DISTINCT keyword or ends in LIMIT 1.
• It projects unique key column(s) from every table in FROM, e.g., SELECT UId, Name FROM Users. • It is constrained by uniqueness in its WHERE clause; e.g.: Events e , Attendances a WHERE e. EId = a. EId AND a. UId = 2 For this query to return multiple copies of x, the database must contain multiple rows of the form Attendances(2, x, ?); this is ruled out by the uniqueness constraint on (UId, EId). In our experience, policy views can typically be written as basic queries directly-e.g., for Listing 1 we can frame V 3 and V 4 as equivalent basic queries by replacing subqueries with joins and using the inner join transformation from §5.2.2.

Rewriting Into Basic Queries
When the application issues a query Q, Blockaid attempts to rewrite it into a basic query Q and verify its compliance instead. Ideally, Q would be equivalent to Q, but when this is not possible, Blockaid produces an approximate Q that reveals at least as much information as Q does. 5 Such approximation preserves soundness but may sacrifice completeness, although it caused no false rejections in our evaluation. We now explain how to rewrite several types of queries encountered in practice. Inner joins. A query of the form: is equivalently rewritten as the basic query: Left joins on a foreign key. Consider a query of the form: A is a foreign key into R2.B, then every row in R1 matches at least one row in R2. In this case, the left join can be equivalently written as an inner join, which is handled as above.
Order-by and limit. We add any ORDER BY column as an output column and then discard the ORDER BY clause. We also discard any LIMIT clause but, when adding this query to the trace, use a modified condition O i ⊆ D(Q i ) (instead of "=") to indicate that Blockaid may have observed a partial result. 4 The MINUS operator is not used in our applications and is omitted. 5 It suffices to guarantee that Q can be computed from the result of Q .
Aggregations. We rewrite SELECT SUM(A) FROM R into SELECT PK, A FROM R, where PK is table R's primary key. By projecting the primary key in addition to A, the rewritten query reveals the multiplicity of the values in A-necessary for computing SUM(A)-without returning duplicate rows. Left joins that project one table. Left joins of the form: can be equivalently rewritten to the basic query: where C3 is obtained by replacing each occurrence of B.? with NULL in C2 and simplifying the resulting predicate. 6 The first sub-query covers the rows in A with at least one match in B, and the second sub-query, those with no matches. Feature not supported. The SQL features that we do not support include GROUP BY, ANY, EXISTS, etc., although they can also be formulated / approximated using basic queries. In the future we also plan to leverage other formalisms that model complex SQL semantics more precisely [14,18,19,[68][69][70]72].

Optimizations and SMT Encoding
We end this section with several optimizations for compliance checking and some notes on the SMT encoding. Strong compliance. We define a stronger notion of compliance, which we found SMT solvers can verify more efficiently.
if for each pair of databases D 1 , D 2 that conform to the schema and satisfy: Q is also compliant, let D 1 , D 2 be databases that satisfy Equations (1) to (3) from the compliance definition. These imply the strong compliance assumptions (Equations (4) and (5)), and so we have Q(D 1 ) ⊆ Q(D 2 ). By symmetry, we also have Q(D 2 ) ⊆ Q(D 1 ). Putting the two together, we conclude Q( showing Q to be compliant to V given T . For faster checking, Blockaid verifies strong compliance rather than compliance; by Theorem 5.5, soundness is preserved. However, there are scenarios where a query is compliant but not strongly compliant (see Appendix B); such queries will be falsely rejected by Blockaid. This did not pose a problem in practice as we found the two notions to coincide for every query encountered in our evaluation. Fast accept. Given a view SELECT C1, ..., Ck FROM R, any query that references only columns R.C1, . . . , R.Ck must be compliant and is accepted without SMT solving. Trace pruning. Queries that returns many rows can inflate the trace and slow down the solvers. Fortunately, often times only few of the rows matter to a later query's compliance. We thus use a trace-pruning heuristic: When checking a query Q, look for any previous query has returned over ten rows, and only keep rows that contain the first occurrence of a primary-key value (e.g., user ID) that appears in Q. This heuristic is sound but may need to be adapted for any application where our premise for pruning does not hold. SQL types and predicates. To model SQL types, we use SMT's uninterpreted sorts, which we found to yield better performance than theories of integers, strings, etc. We support logical operators AND and OR, comparison operators <, <=, >, >=, and operators IN, NOT IN, 7 IS NULL, and IS NOT NULL. We model < as an uninterpreted function with a transitivity axiom. NULLs. We model NULL using a two-valued semantics of SQL [33, § 6] by (1) designating a constant in each sort as NULL, and (2) taking NULL into account when implementing SQL operators. For example, the SQL predicate x=y translates into the following SMT formula: x = y ∧ x = null ∧ y = null.

Decision Generalization and Caching
While SMT solvers can verify a wide range of queries, doing so often takes 100s of milliseconds per query. As a page load can depend on tens of queries, this overhead can add up to seconds.
To alleviate this overhead, Blockaid aims to reduce solver calls by caching compliance decisions. Naively, once query Q is deemed compliant given trace T , we could record (Q, T ) and allow future occurrences without re-invoking the solvers.
However, this proposal is unlikely to be effective because the number of distinct (Q, T ) pairs can be unbounded. For example, the application can issue as many queries of the form SELECT * FROM Users WHERE UId = ? as there are users in the system. Therefore, requiring an exact query-trace match for a cache hit would result in a low cache hit rate. Fortunately, while an application can issue an unbounded number of distinct queries, it only exhibits a finite number of truly different behaviors. For example, the query sequences generated by requests for two different calendar events are likely identical in structure while differing only in parameters (e.g., event ID). If one sequence is compliant, we can generalize this knowledge to conclude that the other is also compliant.
This generalization problem is the central challenge we tackle in this section: Given a query compliant with respect to a trace, how to abstract this knowledge into a decision template such that (1) any query (and its trace) that matches this template is compliant, and (2) the template is general enough to produce matches on similar requests. Such a template, once cached, will apply to an entire class of traces and queries. We do not cache or generalize non-compliance decisions, which are less performance-sensitive as they typically indicate a bug in the application to be fixed by human intervention.
Let us start with an example of a decision template.

Example
Suppose a user with UId = 1 requests Event #42 in the calendar application, resulting in the application issuing a sequence of SQL queries. Consider the third query, shown in Listing 2a. As we explained in Example 4.2, Query #3 is compliant because Query #2 has established that the user attends the event.
Blockaid aims to abstract this query (with trace) into a decision template that applies to another user viewing a different event. Listing 2b shows such a template; the notation says: If each query-output pair above the line has a match in a trace T , then any query of the form below the line is compliant given T .
This particular template states: After it is determined that user x attends event y, user x can view event y for any x and y.
Compared with the concrete query and trace, this template (1) omits Query #1, which is immaterial to the compliance decision; and (2) replaces the concrete values with parameters. Occurrences of ?0 here constrain the event ID fetched by the query to equal the previously checked event ID. We use * to denote a fresh parameter, i.e., any arbitrary value is allowed.
We now dive into how Blockaid extracts such a decision template from a concrete query and trace. But before we do so, let us define what a decision template is, what it means for a template to have a match, and what makes a "good" template.

Definitions and Goals
For convenience, from now on we will denote a trace as a set of query-tuple pairs {(Q i ,t i )} n i=1 , where each t i is one of the rows returned by Q i . A query that returns multiple rows is represented as multiple such pairs. This change of notation is permissible because under strong compliance (Definition 5.4), we no longer take into account the absence of a returned row. • Q D is the parameterized query, whose definition can refer to variables from x ∪ c; • T D is the parameterized trace, whose queries and tuples can refer to variables from x ∪ c; and • Φ D , the condition, is a predicate over x ∪ c.
We often denote a template simply by D if the variables are either obvious from context or unimportant. to objects that contain variables in y. For example, given a parameterized query Q, ν(Q) denotes Q with each occurrence of variable y ∈ y substituted with ν(y). • (ν(Q j ), ν(t j )) ∈ T for all (Q j ,t j ) ∈ T D , and • ν(Φ D ) holds. We are interested only in templates that imply compliance. Definition 6.6. A decision template D is sound with respect to a policy V if for every request context ctx, whenever D matches (Q, T ) under ctx, Q is strongly ctx-compliant to V given T .
For a compliant query Q (with trace T ) that misses the cache, there often exist many sound templates that match (Q, T ). But all such templates are not equal-we prefer the more general ones, those that match a wider range of other query-trace pairs. Definition 6.7. A template D 1 is at least as general as a template D 2 if for every query Q and feasible trace T , if D 2 matches (Q, T ), D 1 also matches (Q, T ).

Thus, Blockaid aims to generate a decision template that
(1) is sound, (2) matches (Q, T ), and (3) is general enough for practical purposes. We now explain how this is achieved.

Generating Decision Templates
Blockaid starts from the trivial template D 0 = (Q, T , ), which is sound but not general, and generalizes it in two steps: 1. Minimize the trace T to retain only those (Q i ,t i ) pairs that are required for Q's compliance ( §6.3.1).

Replace each constant in the trace and query with a fresh
variable, and then generate a weak condition Φ over the variables that guarantees compliance ( §6.3.3).

Step One: Trace Minimization
Blockaid begins by finding a minimal sub-trace of T that preserves compliance. It removes each (Q i ,t i ) ∈ T and, if Q is no longer compliant, adds the element back. For example, for Listing 2a this step removes Query #1. Denote the resulting minimal trace by T min and let decision template D 1 = (Q, T min , ).
Proposition 6.8. D 1 is sound, matches (Q, T ), and is at least as general as D 0 .
As an optimization, Blockaid starts the minimization from the sub-trace that the solver has actually used to prove compliance. It extracts this information from a solver-generated unsat core [8, § 11.8]-a subset of clauses in the formula that remains unsatisfiable even with all other clauses removed. If we attach labels to the clauses we care about, a solver will identify all labels in the unsat core when it proves the formula unsatisfiable.
To get an unsat core, Blockaid uses the following formula: where the clause asserting the i th trace entry is labeled LQ i . If Q is compliant, the solver returns as the unsat core a set S of labels. Blockaid ignores any (Q i ,t i ) ∈ T for which LQ i ∈ S.

Interlude: Model Finding for Satisfiable Formulas
A common operation in template generation is to remove parts of a formula and re-check satisfiability. A complication arises when the formula turns satisfiable-while solvers are adept at proving unsatisfiability, they often fail on satisfiable formulas. 8 To solve these formulas faster, we observe that they are typically satisfied by databases with small tables. We thus construct SMT formulas to directly seek such "small models" by representing each table not as an uninterpreted relation, but as a conditional table [37] whose size is bounded by a small constant.
A conditional table generalizes a regular table by (1) allowing variables in its entries, and (2) associating with each row with a condition, i.e., a Boolean predicate for whether the row exists. For example, a Users table with a bound of 2 appears as: UId Name Exists?
where each entry and condition is a fresh variable, signifying that the table is not constrained in any way other than its size. Queries on condition tables can be evaluated via an extension of the relational algebra operators [37, § 7]. This allows queries to be translated into SMT without using quantifiers or relation symbols. For example, the query SELECT Name FROM Users WHERE UId = 5 can be written as: We found that such formulas could be solved quickly by Z3.
After Blockaid uses the regular (unbounded) formula to generate an unsat core S ( §6.3.1), it switches to using bounded formulas for the remainder of template generation. Blockaid sets a table's bound to one plus the number of rows required to produce the sub-trace induced by S; 9 it relies on the solvers to produce small unsat cores to keep formula sizes manageable.
Care must be taken because using bounded formulas breaks soundness-a query compliant on small tables might not be on larger ones. Therefore, after a decision template is produced Blockaid verifies its soundness on the unbounded formula, and if this fails, increments the table bounds and retry.

Step Two: Find Value Constraints
Taking the template D 1 = (Q, T min , ) from Step 1, Blockaid generalizes it further by abstracting away the constants. To do so, Blockaid parameterizes T min and Q by replacing each occurrence of a constant with a fresh variable. We use a superscript "p" to denote the parameterized version of a query, tuple, or trace. Listing 3a shows T p min and Q p from our example. As an optimization, Blockaid assigns the same variable (e.g., x0) to locations that are guaranteed by SQL semantics to be equal.
Blockaid must now generate a condition Φ such that the resulting template D 2 = (Q p , T p min , Φ) meets our goals. It picks as Φ a conjunction of atoms from a set of candidate atoms. Let x denote all variables generated from parameterization, and let ν map x to the replaced constants and c to the current context ctx. Definition 6.9. The set of candidate atoms is defined as: . 9 If the bounds are too small for a database to produce the trace, the resulting formula will be unsatisfiable regardless of compliance. Form x = v: (We write atoms in monospace font to distinguish them from mathematical expressions. Following SQL, the "=" in an atom implies that both sides are non-NULL.) Note that all atoms hold on Q and T min . Blockaid now selects a subset that not only guarantees compliance, but also imposes relatively few restrictions on the variables. Definition 6.10. With respect to Q p and T p min , a subset of ( C 0 denotes the conjunction of atoms in C 0 .) Definition 6.11. Let C 1 ,C 2 ⊆ C. We say that C 2 is at least as weak as C 1 if C 1 =⇒ C 2 , and that C 2 is weaker than C 1 if C 2 is at least as weak as C 1 but not vice versa. Example 6.12. Listing 3b shows all the candidate atoms from Listing 3a (after omitting symmetric ones in the x = x' group). Consider the following two subsets of atoms: While both are sound,C 2 is preferred overC 1 as it is weaker and thus applies in more scenarios. In fact, C 2 is maximally weakthere exists no subset that is both sound and weaker than C 2 .
Ideally, Blockaid would produce a maximally weak sound subset of C as the template condition, but finding one can be expensive. It thus settles with finding a subset that is weak enough for practical generalization. It does so in three substeps.
First, as a starting point, Blockaid generates a minimal unsat core of the formula: LetC core denote the atoms whose label appears in the unsat core.
For example, C core = { MyUId = x0, x1 = 42, x3 = 42 }. Second, it augments C core with other atoms that are implied by it: C aug = { c ∈ C | C core =⇒ c }. In our example, C aug always contains a maximally weak sound subset of C. Thus, Blockaid focuses its search within C aug .
Finally, as a proxy for weakness, Blockaid finds a smallest sound subset of C aug , denoted C small , breaking ties arbitrarily. It does so using the MARCO algorithm [45,46,56] for minimal unsatisfiable subset enumeration, modified to enumerate from small to large and to stop after finding the first sound subset. In our example, the algorithm returns C small = { MyUId=x0, x1=x3 } of cardinality two-which is also a maximally weak subset-even though this might not be the case in general. 10 Nevertheless, searching for a smallest sound subset has produced templates that generalize well in practice.
Blockaid thus produces the decision template: Proposition 6.13. D 2 is sound, matches (Q, T ), and is at least as general as D 1 .
As an optimization, whenever C small =⇒ x = y for x, y ∈ x ∪ c, Blockaid replaces x with y in the template. This is how, e.g., ?0 appears both in the trace and the query in Listing 2b.

Optimizations
We implement two optimizations that improve the performance of template generation and the generalizability of templates.
Omit irrelevant tables. Given trace T and query Q, we call a table relevant if (1) it appears in T or Q, or (2) the table appears on the right-hand side of a database constraint of the form Q 1 ⊆ Q 2 , given that a relevant table appears on the left. 11 Blockaid sets the size bounds of irrelevant tables to zero, reducing formula size while preserving compliance. Split IN. A query Q that contains " c IN (x 1 , x 2 , . . . , x n )" often produces a template with a long trace. If Q is a basic query that does not contain the NOT operator, it can be split into q 1 , . . . , q n where q i denotes Q with the IN-construct substituted with c = x i , such that Q ≡ q 1 ∪ . . . ∪ q n . If q 1 , . . . , q n are all compliant then so is Q, and so Blockaid checks the sub-queries instead. This is usually fast because q 2 , . . . , q n typically match the decision template generated from q 1 . If any q i is not compliant, Blockaid reverts to checking Q as a whole.
This optimization also improves generalization. Suppose Q has structure identical to Q but a different number of IN operands. It would not match a template generated from Q, but its split sub-queries q i could match the template from q 1 .

Decision Cache and Template Matching
Blockaid stores decision templates in its decision cache, indexing them by their parameterized query using a hash map. When checking a query Q, Blockaid lists all templates whose parameterized query matches Q; for each template, it uses recursive backtracking (with pruning optimizations) to search for a valuation that results in a match. This simple method proves efficient in practice as templates generated by Blockaid tend to be small.

Implementation
We implemented Blockaid as a Java Database Connectivity (JDBC) driver that interposes on an underlying connection. It thus supports only applications on the JVM and runs within the web server, although our design allows it to reside elsewhere (e.g., in the database). The JDBC driver accepts custom commands that (1) set the request context, (2) clear the context and the trace, and (3) check an application cache read.
Blockaid parses SQL using Apache Calcite [9] and caches parser outputs. To check compliance, it uses Z3's Java binding [25] to generate formulas in SMT-LIB 2 format [7] and invokes an ensemble of solvers in parallel. Our ensemble consists of Z3 [26] (v4.8.12) and CVC5 [6] (v0.3) using default configurations, and Vampire [42] (v4.6.1) using six configurations from its CASC portfolio. 12 The ensemble is killed as soon as any solver finishes. If a query is not compliant, or all solvers time out after 5 s, Blockaid throws a Java SQLException.
To generate decision templates, Blockaid uses the same ensemble to produce the initial unsat core ( §6.3.1), but kills the ensemble only when a solver returns a small core of up to 3 labels (subject to timeout). It uses only Z3 on bounded formulas.
Our prototype does not verify that queries return no duplicate rows and does not look at any ORDER BY columns. We manually ensured that queries in our evaluation return no duplicates and do not reveal inaccessible information through ORDER BY.

Evaluation
We use Blockaid to enforce data-access policies on three existing open-source web applications written in Ruby on Rails: • diaspora* [27]: a social network with 850 k users.
• Autolab [5]: a course management app used at 20 schools. For each application, we devised a data-access policy, modified its code to work with Blockaid, and measured its performance. In summary, Blockaid imposes overheads of 2.2 %-8.3 % to the median page load time when compliance decisions are cached, and the decision templates produced by Blockaid generalize to other entities (users, posts, etc.  Figure 2: URL fetch latency (median). With all compliance decisions cached, Blockaid incurs up to 10 % overhead over "modified".  Table 1 summarizes the constraints and policies for database tables queried in our benchmark, including any necessary application-level constraints (e.g., a reshared post is always public in diaspora*). Spree and Autolab use the Rails cache, and we annotate their cache key patterns with queries ( §3.2). Once a policy is given, transcribing it into views was straightforward. The more arduous task lied in divining the intended policy for an application, by studying its source code and interacting with it on sample data. This effort was complicated by edge cases in policies-e.g., a Spree item at an inactive location is inaccessible except when filtering for backorderable variants. Such edge cases had to be covered using additional views.

Constraints, Policies, and Annotations
To give a sense of the porting effort, writing the Spree policy took one of us roughly a month. However, this process would be easier for the developer of a new application, who has a good sense of what policies are suitable and can create policies while building the application, amortizing the effort over time.
When writing the Autolab policy, we uncovered two accesscheck bugs in the application: (1) a persistent announcement (one shown on all pages of a course) is displayed regardless of whether it is active on the current date; and (2) an unreleased handout is hidden on its course page but can be downloaded from its assignment page. This experience corroborates the difficulty of making every access check airtight, especially for code bases that enjoy fewer maintenance resources.

Code Modifications
Our changes to application code fall into five categories: 1. Boilerplate: We add code that sends the request context to Blockaid at request start and clears the trace at request end. 2. Fetch less data: We modify some queries to not fetch potentially sensitive data unless it will be revealed to the user; some of these changes use the lazy_column gem [47]. 3. SQL features: We modify some queries to avoid SQL features not supported by Blockaid (e.g., general left joins) without altering application behavior. 4. Parameterize queries: We make some queries parameterized so that Blockaid can effective cache their parsing results. Most changes are mechanical rewrites of queries with comparisons, as idiomatic ways of writing comparisons [55] cause query parameters to be filled within Rails. 5. File system checking: Autolab uses files to store submissions; the file name are always accessible but the content is inaccessible during an exam. We modify it to store the submission content under a randomly generated file name and restrict access to the file name in the database ( §3.2). The code changes are summarized also in Table 1, which omits configuration changes, adaptations for JRuby, and experiment code. The changes range from 19 to 96 lines of code.

Experiment Setup and Benchmark
We deploy each application on an Amazon EC2 c4.8xlarge instance running Ubuntu 18.04. Because our prototype only supports applications on the JVM ( §7), we run the applications using JRuby [38] (v9.3.0.0), a Ruby implementation atop the JVM (we use OpenJDK 17). In Rails's database configuration, we enable the prepared_statements option so that Rails issues parameterized queries in the common case. 13 The For each application, we picked five page loads that exercise various behaviors (Table 2). Each page load can fetch multiple URLs, some common among many pages (e.g., D9, which is the notifications URL). All queries issued are compliant, and all experiments are performed with the Rails cache populated.

Page Load Times
We start by measuring the page load time (PLT) using a headless Chrome browser (v96) driven by Selenium [64]. The PLT is reported as the time elapsed between navigationStart and loadEventEnd as defined by the PerformanceTiming interface [73]. The one exception is the Autolab "Submission" page, a file download, for which we report Chrome's download time instead. Since the client is on the same VM as the server, these experiments reflect the best-case PLT, as clients outside the instance / cloud are likely to experience higher network latency.
We report the PLT under four settings: "Original" (unmodified application), "Modified" (applications modified à la §8.2), "Cached" (modified application under Blockaid with every query hitting the decision cache), and "No cache" (decision caching disabled). For the first three settings, we perform 3000 warmup loads before measuring the PLT of another 3000 loads. For "no cache", where each run lasts longer, we use 100 warmup loads and 100 measurement loads. Table 2 shows that when compliance decisions are cached, Blockaid incurs up to 12 % overhead to median PLT over the modified application (and up to 17 % overhead to P95). With caching disabled, Blockaid incurs up to 236× higher median PLT. Compared with the original applications, the modified versions result in up to 6 % overhead to median PLT for all pages but Autolab's "Submissions", which suffers a 19 % overhead. (The P95 overhead is up to 7 % for all but two pages with up to 26 % overhead.) We will comment on these overheads in the next subsection, where we break down the pages into URLs.

Fetch Latency
To better understand page load performance, we separate out the individual URLs fetched by each page (Table 2), omitting URLs for assets, and measure the latency of fetching each URL (not including rendering time). The median latencies are shown in Figure 2. In addition to the four settings from §8.4, it includes performance under a "cold cache", where the decision cache is enabled but cleared at the start of each load (100 warmup runs followed by 100 measurements). When all compliance decisions are cached, Blockaid incurs up to 10 % of overhead (median 7 %) over "modified". In contrast, it incurs 7×-422× overhead on a cold decision cache, and 7×-310× overhead if the decision cache is disabled altogether.
For most URLs, "cold cache" is slower than "no cache" due to the extra template-generation step. Two exceptions are D4 and A6, where many structurally identical queries are issued. As a result, the performance gain from cache hits within each URL offsets the performance hit from template generation. Compared to the original, the modified diaspora* and Spree are up to 5 % slower (median 2 %), but the Autolab overhead is up to 21 % (median 8 %). This is because Autolab routinely reveals partial information on objects that are not fully accessible. For example, it allows a user to distinguish among the cases where: (1) a course doesn't exist, (2) a course exists but the user is not enrolled, and (3) the user is enrolled but the course is disabled. The original Autolab fetches the course in one SQL query but we had to split it into multiple-checking whether the course exists, whether it is disabled, etc.-and return an error immediately if one of these checks fails.
In one instance (S2), the modified version is 11 % faster than the original because we were able to removed queries for potentially sensitive data that is never used in rendering the URL.

Solver Comparison
When a query arrives, Blockaid invokes an ensemble of solvers to check compliance when decision caching is disabled, and to generate a decision template on a cache miss when caching is enabled. The winner, in the no-cache case, is the first solver to return a decision; and in the cache-miss case, the first to return a small enough unsat core ( §7), assuming the query is compliant. Figure 3 shows the fraction of wins by each solver in the two scenarios. In the no-cache case, wins are dominated by Z3 followed by CVC5, with none for Vampire. In the cache-miss case, however, Vampire wins a significant portion of the time-Z3 and CVC5 often finish quickly but with large unsat cores, causing Blockaid to wait till Vampire produces a smaller core.

Template Generalization
We found that the generated decision templates typically generalize to similar requests. The rest generalize in more restricted scenarios, but none is tied to a particular user ID, post ID, etc.
To illustrate how Blockaid might produce a template that does not generalize fully, consider a query from Spree's cache key annotations (Listing 4). This query fetches assets for product variants in the user's order; here, a variant's asset belongs to its product's "master variant". Listing 4a shows a template that fails to generalize fully, for three reasons.
First, due to the queries with the IN operator in its premise (above the horizontal line), this template only applies when an order has exactly three variants. The IN-splitting optimization from §6.3.4 only applies to the query being checked, and we plan to handle such queries in the premise in future work.
Second, this template constrains the variant to be "not discontinued", which Spree defines as discontinue_on IS NULL or discontinue_on >= NOW. But because disjunctions are not supported in decision templates, Blockaid picked only the condition that matches the current variant (IS NULL).
Third, in this example there are multiple justifications for this query's compliance, and Blockaid happened to pick one that does not always hold in a similar request. The policy states that a variant's asset can be viewed if it is not discontinued, or if it is part of the user's order. 14 This particular variant in the user's order happens to not be discontinued, and the template captures the former justification for viewing the asset. However, it does not apply to variants in the order that are discontinued; indeed, for such a variant, Blockaid produces the template in Listing 4b, which generalizes fully. We could address this issue by finding multiple decision templates for every query.
Incidentally, inspecting decision templates has helped us expose overly permissive policies. When writing the Autolab policy we missed a join condition in a view, a mistake that became apparent when Blockaid generated a template stating that an instructor for one course can view assignments for all courses. Decision templates show consequences of a policy, and more general templates are more likely to reveal undesired consequences of an overly broad policy.

Discussions and Future Work
Comparison to row-and cell-level policy. A popular form of data-access policies alternative to the view-based variety is row-and/or cell-level policies, implemented in databases like SQL Server [50] and Oracle [53]. Such policies are less expressive than views and fail to cover many practical cases.
For example, suppose we wish to allow each user to view everyone's timetables (i.e., the start and end times of the events they attend). Querying someone's timetable requires joining the Events and Attendances tables on the EId column, which must then be treated as visible by a cell-level policy. But this inevitably reveals meeting attendee information as well. Instead, we can implement this policy using a view: Blockaid can now ask whether the user attends Event #5 and if so, allow the query. In fact, under this setup the "sufficientand-necessary" condition for application noninterference (in the sense of §4.3) becomes instance-based determinacy [41,60,75], a criterion less stringent than trace determinacy. We decided against granting this ability to Blockaid for two reasons. First, it seems nontrivial to check instance-based determinacy efficiently-Blockaid must either figure out a minimal set of queries to ask, a difficult problem, or fetch all accessible information, an expensive task. Second, Blockaid is designed for conventional web applications that do not rely on an enforcer for data-access compliance. Such applications should not be issuing queries that fail trace determinacy but pass instance-based determinacy: Such queries can reveal inaccessible information on a different database in Blockaid's absence and typically indicate bugs in application code. Thus, Blockaid is right to flag them.
Theoretically optimal template generalization. Although decision templates generated by Blockaid are general enough in practice, they are not guaranteed to be maximally general among the templates that match the query and trace being checked. For one thing, the template condition generated might not be maximally weak ( §6.3.3). For another, a maximally general template can have a longer trace than the concrete one, a possibility that Blockaid never explores.
Fundamentally, Blockaid's decision template generation algorithm is limited by its black-box access to the policy-i.e., the algorithm interacts with the policy solely via checking template soundness using SMT solvers. Producing theoretically optimal templates might require opening up this black box and having the policy guide template generation more directly, a path we intend to explore in future work.

Conclusion
Blockaid is a dynamic data-access enforcement system that supports existing web frameworks. It uses SMT solvers to check compliance against view-based policies, and uses a novel caching technique to achieve low performance overhead. We hope that the approach taken by Blockaid can help rule out data-access bugs in real-world applications.   Part 2. Suppose E correctly enforces V . Pick any ctx, Q, and prefix E-allowed T = {(Q i ,t i )} n i=1 such that E(ctx, Q, T ) = . Consider the following program P : procedure P (ctx, req, D) for i ← 1..n do issue Q i (D) and discard the result return Q(D) To show that Q is ctx-compliant to V given T , let D and D be databases such that: Let req be any request, and consider executions P E (ctx, req, D) and P E (ctx, req, D ). Because T is prefix E-allowed, neither execution ends in a policy violation error. Therefore, P E (ctx, req, D) = P (ctx, req, D) = Q(D), P E (ctx, req, D ) = P (ctx, req, D ) = Q(D ).
Furthermore, because E correctly enforces V , Equation (8) implies that P E (ctx, req, D) = P E (ctx, req, D ). We thus have Q(D) = Q(D ), concluding Q to be ctx-compliant to V given T .

B From Compliance to Strong Compliance
To understand when strong compliance fails to coincide with compliance, let us look at Figure 4, which illustrates how we modified the definition of compliance (Definition 4.5) into that of strong compliance (Definition 5.4) in five steps.
Step 1 does not affect the truthfulness of the formula since D 1 and D 2 are symmetric. Steps 2-3 adopt an open-world assumption (OWA) [58], treating every query as returning partial results. Under this assumption, a trace can no longer represent the nonexistence of a returned row; this can cause Blockaid may falsely reject a query. However, such cases never arose in our evaluation. The OWA also proves convenient during decision template generation ( §6.3.1) when Blockaid computes a minimal sub-trace (which, by necessity, represents partial information) that guarantees strong compliance.
To see how Step 4 affects the definition, suppose there are no database dependencies and the trace is empty (so Steps 2-3 are irrelevant). In this scenario, compliance holds iff V determines Q [52,62], while strong compliance states that Q has a monotonic rewriting using V . There are cases where determinacy holds but no monotonic rewriting exists; e.g., Nash et al. [52, § 5.1] present an example in terms of conjunctive queries. Finally, in Step 5 we drop the condition that D 2 be consistent with the trace. We can show by induction that this condition is redundant as long as each query in the trace is strongly compliant given the trace before it (which is the case in Blockaid).