Computation over sensitive data requires that the computation function is secure and trusted. Existing approaches either do not enforce formal verification, require the user to verify the proof, or lack secure attestation guarantees. In addition, neither addresses the issue of having users once again inspect the application after upgrading the code running in the enclave. We propose an approach that uses a formal specification to guarantee that the behavior of the computation function conforms to the desired functionality. By combining automated verification with attestation on a trusted execution environment, we ensure that only conformant applications are executed. At the same time, we allow updates of the computation function without changing the attestation response, as long as the formal specification still holds. We implement and evaluate the system on several functions; our results show an average overhead of only 50 %. Finally, we demonstrate the validity of the system using a real-world application, Dafny-EVM.

Many applications benefit from computations over the data of multiple users while preserving confidentiality. We present a solution where multiple mutually distrusting users' data can be aggregated with an acceptable overhead, while allowing users to be added to the system at any time without re-encrypting data. Our solution to this problem is to use a Trusted Execution Environment (Intel SGX) for the computation, while the confidential data is encrypted with the data owner's key and can be stored anywhere, without trust in the service provider. We do not require the user to be online during the computation phase and do not require a trusted party to store data in plain text. Still, the computation can only be carried out if the data owner explicitly has given permission.Experiments using common functions such as the sum, least square fit, histogram, and SVM classification, exhibit an average overhead of 1.6×. In addition to these performance experiments, we present a use case for computing the distributions of taxis in a city without revealing the position of any other taxi to the other parties.

IoT systems, such as in smart cities or hospitals, generate data that may be subject to different security classifications, privacy regulations, and access rights. However, popular IoT platforms do not consider data classification and security-aware data analysis. In this paper, we present a novel architecture based on open-source solutions that handles the issue of collecting and classifying data at the source and presents the data analysis to users at different authorization levels. Our architecture consists of three layers: a layer for exposing collected and classified data to a middleware, the middleware to handle storage and analysis of the data and expose it to a dashboard, and the dashboard responsible for authenticating users and visualizing data according to the users' classification level. Our solution distinguishes itself by focusing on data classification rather than data collection, supporting fine-grained access control and declassification. Our implementation, using the Web of Things API, Node-RED and Grafana, demonstrates the security benefits of our design on use cases in the smart city and healthcare domains.