• Skip to Content
  • Skip to Main Navigation
  • Skip to Search

Indiana University Bloomington Indiana University Bloomington IU Bloomington

Open Search
  • Our people
  • Our research
  • Degree Programs
  • Cybersecurity resources
  • News & Events
    • Cybersecurity in the news

Security and Privacy in
Informatics, Computing, and Engineering

  • Home
  • Our people
  • Our research
  • Degree Programs
  • Cybersecurity resources
  • News & Events
    • Cybersecurity in the news
  • Search
  • Home
  • News & Events
  • News - Manual
  • 2025
  • Hiroki Chen

Cybersecurity Speaker

Image of Hiroki Chen
Hiroki Chen

January 31, 2025

Time: 11:00 AM - 12:30 PM
Location: Luddy Hall 0117
Speaker: Hiroki Chen
Title: PICACHV: Formally Verified Data Use Policy Enforcement for Secure Data Analytics

Abstract:
Ensuring the proper use of sensitive data in analytics under complex privacy policies is an increasingly critical challenge. Many existing approaches lack portability, verifiability, and scalability across diverse data processing frameworks. We introduce PICACHV, a novel security monitor that automatically enforces data use policies. It works on relational algebra as an abstraction for program semantics, enabling policy enforcement on query plans generated by programs during execution. This approach simplifies analysis across diverse analytical operations and supports various front-end query languages. By formalizing both data use policies and relational algebra semantics in Coq, we prove that PICACHV correctly enforces policies. PICACHV also leverages Trusted Execution Environments (TEEs) to enhance trust in runtime, providing provable policy compliance to stakeholders that the analytical tasks comply with their data use policies. We integrated PICACHV into Polars, a state-of-the-art data analytics framework, and evaluate its performance using the TPC-H benchmark. We also apply our approach to real-world use cases. Our work demonstrates the practical application of formal methods in securing data analytics, addressing key challenges.

Security and Privacy in Informatics, Computing, and Engineering resources

  • Luddy School of Informatics, Computing, and Engineering

Indiana University

Accessibility | College Scorecard | Privacy Notice | Copyright © 2025 The Trustees of Indiana University