FastVer is a protocol that uses a variety of memory-checking techniques to monitor the integrity of key-value stores with only a modest runtime cost. Arasu et al. formalize the high-level design of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct implementation---FastVer is implemented in unverified C++ code. In this work, we present FastVer2, a low-level, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to FastVer's high-level specification. Our proof is the first end-to-end system proven using Steel, and in doing so we contribute new ghost-state constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer. We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement, and expect to address these in the future.

Inference attacks on property-preserving encrypted databases (e.g., CryptDB) have been previously studied. These demonstrate how in certain scenarios one can recover plain text from databases that provide columnar encryption by using auxiliary information such as column statistics. Newer generation of encrypted databases are now being built using secure enclave technology. In this paper, we first show how the current generation of encrypted databases are robust against these previously published attacks. However, we identify two broad patterns that we identify as query integrity attacks and data integrity attacks that can be used to construct attacks that are similar in scope for a variety of encrypted databases built using enclaves. We believe this paper initiates an important discussion about the need for integrity protection for future encrypted databases.

We present FastVer, a high-performance key-value store with strong data integrity guarantees. FastVer is built as an extension of FASTER, an open-source, high-performance key-value store. It offers the same key-value API as FASTER plus an additional verify() method that detects if an unauthorized attacker tampered with the database and checks whether results of all read operations are consistent with historical updates. FastVer is based on a novel approach that combines the advantages of Merkle trees and deferred memory verification. We show that this approach achieves one to two orders of magnitudes higher throughputs than traditional approaches based on either Merkle trees or memory verification. We have formally proven the correctness of our approach in a proof assistant, ensuring that verify() detects any inconsistencies, except if a collision can be found on a cryptographic hash.

The uses of web search engines are very frequent and common worldwide over the internet by end users for different purposes. A web search engine takes the query request from the end user and executes that query on relational database used to store the information on behalf of that web search engine. Based on input queries the dynamic response is generated by search engine, in the form of HTML based pages. Such pages are supported with the web databases. Every web page generated contains many results to display for particular query, called as Search Result Records (SRRs). Sometimes it becomes troublesome to extract relevant data from diverse sources. The SRRs generated may contain data units that are relevant to one common semantic. These SRRs are further required to be assigned with proper labels. The manual methods for record extraction and labeling have a worse scalability. Thus automatic annotation based method is needed to improve the accuracy as well as scalability of web search engines. This paper presents an automatic annotation technique for web search results. The proposed approach first aligns the data units on a result page into different groups such that the data in the same group have the same semantic. Then, each group is annotated from different aspects and aggregates the different annotations to predict a final annotation label for it. The annotation wrapper generated for the search site is automatically constructed and can be used to annotate new result pages from the same web database. Experiments indicate that

This paper presents Always Encrypted, a recently released feature of Microsoft SQL Server that uses column granularity encryption to provide cryptographic data protection guarantees. Always Encrypted can be used to outsource database administration while keeping the data confidential from an administrator, including cloud operators. The first version of Always Encrypted was released in Azure SQL Database and as part of SQL Server 2016, and supported equality operations over deterministically encrypted columns. The second version, released as part of SQL Server 2019, uses an enclave running within a trusted execution environment to provide richer functionality that includes comparison and string pattern matching for an IND-CPA-secure (randomized) encryption scheme. We present the security, functionality, and design of Always Encrypted, and provide a performance evaluation using the TPC-C benchmark.

Deferred verification of the integrity of data operations over a set of data that is hosted at an untrusted module (UM) is controlled. The controlling includes generating a request for a data operation on the set of data. The request includes an authentication portion. The request is sent to the UM. A response to the request is received from the UM. The response includes cryptographic verification information attesting the integrity of the data operation with respect to prior data operations on the set of data. The response includes results from deferred verification at a trusted module (TM).

In this paper we present BlockchainDB , which leverages blockchains as a storage layer and introduces a database layer on top that extends blockchains by classical data management techniques (e.g., sharding) as well as a standardized query interface to facilitate the adoption of blockchains for data sharing use cases. We show that by introducing the additional database layer, we are able to improve the performance and scalability when using blockchains for data sharing and also massively decrease the complexity for organizations intending to use blockchains for data sharing.

In this demo we present BlockchainDB, which leverages blockchains as storage layer and introduces a database layer on top that extends blockchains by classical data management techniques (e.g., sharding). Further, BlockchainDB provides a standardized key/value-based query interface to facilitate the adoption of blockchains for data sharing use cases. With BlockchainDB we can thus not only improve the performance and scalability of blockchains for data sharing but also decrease the complexity for organizations intending to use blockchains for this use case.

In this paper we present BlockchainDB, which leverages blockchains as a storage layer and introduces a database layer on top that extends blockchains by classical data management techniques (e.g., sharding) as well as a standardized query interface to facilitate the adoption of blockchains for data sharing use cases. We show that by introducing the additional database layer, we are able to improve the performance and scalability when using blockchains for data sharing and also massively decrease the complexity for organizations intending to use blockchains for data sharing.

In this paper we introduce shared, verifiable database tables, a new abstraction for trusted data sharing in the cloud.

Encrypted databases have been studied for more than 10 years and are quickly emerging as a critical technology for the cloud. The current state of the art is to use property-preserving encrypting techniques (e.g., deterministic encryption) to protect the confidentiality of the data and support query processing at the same time. Unfortunately, these techniques have many limitations. Recently, trusted computing platforms (e.g., Intel SGX) have emerged as an alternative to implement encrypted databases. This paper demonstrates some vulnerabilities and the limitations of this technology, but it also shows how to make best use of it in order to improve on confidentiality, functionality, and performance.

Verifying the integrity of outsourced data is a classic, well-studied problem. However current techniques have fundamental performance and concurrency limitations for update-heavy workloads. In this paper, we investigate the potential advantages of deferred and batched verification rather than the per-operation verification used in prior work. We present Concerto , a comprehensive key-value store designed around this idea. Using Concerto, we argue that deferred verification preserves the utility of online verification and improves concurrency resulting in orders-of-magnitude performance improvement. On standard benchmarks, the performance of Concerto is within a factor of two when compared to state-of-the-art key-value stores without integrity.

Traditional database management systems are best equipped to run one-time queries over finite stored data sets. However, many modern applications such as network monitoring, financial analysis, manufacturing, and sensor networks require long-running, or continuous, queries over continuous unbounded streams of data. In the STREAM project at Stanford, we are investigating data management and query processing for this class of applications. As part of the project we are building a general-purpose prototype Data Stream Management System (DSMS), also called STREAM, that supports a large class of declarative continuous queries over continuous streams and traditional stored data sets. The STREAM prototype targets environments where streams may be rapid, stream characteristics and query loads may vary over time, and system resources may be limited.

Cipherbase is a comprehensive database system that provides strong end-to-end data confidentiality through encryption. Cipherbase is based on a novel architecture that combines an industrial strength database engine (SQL Server) with lightweight processing over encrypted data that is performed in secure hardware. The overall architecture provides significant benefits over the state-of-the-art in terms of security, performance, and functionality. This paper presents a prototype of Cipherbase that uses FPGAs to provide secure processing and describes the system engineering details implemented to achieve competitive performance for transactional workloads. This includes hardware-software co-design issues (e.g. how to best offer parallelism), optimizations to hide the latency between the secure hardware and the main system, and techniques to cope with space inefficiencies. All these optimizations were carefully designed not to affect end-to-end data confidentiality. Our experiments with the TPC-C benchmark show that in the worst case when all data are strongly encrypted, Cipherbase achieves 40% of the throughput of plaintext SQL Server. In more realistic cases, if only critical data such as customer names are encrypted, the Cipherbase throughput is more than 90% of plaintext SQL Server.

Motivated by cloud security concerns, there is an increasing interest in database systems that can store and support queries over encrypted data. A common architecture for such systems is to use a trusted component such as a cryptographic co-processor for query processing that is used to securely decrypt data and perform computations in plaintext. The trusted component has limited memory, so most of the (input and intermediate) data is kept encrypted in an untrusted storage and moved to the trusted component on ``demand.'' In this setting, even with strong encryption, the data access pattern from untrusted storage has the potential to reveal sensitive information; indeed, all existing systems that use a trusted component for query processing over encrypted data have this vulnerability. In this paper, we undertake the first formal study of secure query processing, where an adversary having full knowledge of the query (text) and observing the query execution learns nothing about the underlying database other than the result size of the query on the database. We introduce a simpler notion, oblivious query processing, and show formally that a query admits secure query processing iff it admits oblivious query processing. We present oblivious query processing algorithms for a rich class of database queries involving selections, joins, grouping and aggregation. For queries not handled by our algorithms, we provide some initial evidence that designing oblivious (and therefore secure) algorithms would be hard via reductions from two simple, well-studied problems that are generally believed to be hard. Our study of oblivious query processing also reveals interesting connections to database join theory.

The subject disclosure is directed towards secure query processing over encrypted database records without disclosing information to an adversary except for permitted information. In order to adapting semantic security to a database encryption scheme, a security model for all query processing is specified by a client and used to determine which information is permitted to be disclosed and which information is not permitted. Based upon the security model, a trusted, secure query processor transforms each query and an encrypted database into secure query results. Even though the adversary can view the secure query results during communication to the client, the adversary cannot determine any reliable information regarding the secure query results or the encrypted database.