Ph.D. Candidate at JAIST

Seungil Yang

Formal verification of privacy and identity disclosure in data and AI systems

I study how privacy leakage and re-identification risks can be modeled, explained, and verified before deployment using relational logic, model checking, and system-level reasoning.

My current work frames identity disclosure as a relational reachability problem and extends design-time privacy verification toward LLM and RAG systems.

Formal Methods Privacy & Security LLM / RAG Systems Model Checking

View Publications Contact Download CV

About

I am a Ph.D. candidate in Transdisciplinary Sciences at JAIST. My research focuses on the formal modeling and verification of identity disclosure, privacy leakage, and re-identification risks in data and AI systems.

I develop verification frameworks that analyze whether a given data release, de-identification policy, or system behavior can logically lead to privacy disclosure. My work aims to bridge empirical privacy evaluation and formal assurance.

Research Focus

Privacy Verification

Formal analysis of disclosure and re-identification risks at design time.

Relational Reachability

Modeling privacy leakage as reachability through transformations and attacker inference.

Healthcare Data

Studying re-identification risks in sensitive healthcare and structured data settings.

LLM / RAG Security

Extending formal privacy reasoning to retrieval, generation, memory, and contextual leakage.

Research Interests

My research aims to establish a formal foundation for privacy and security in data-driven systems. I model identity disclosure as a relational reachability problem, where privacy is defined as the inability to reach identifiable states through data transformations and inference processes.

This perspective enables design-time verification of privacy risks and provides a rigorous alternative to purely heuristic or statistical approaches. I am particularly interested in connecting formal verification with privacy benchmarking and auditing in LLM and RAG systems.

Methodology

I use Alloy and relational logic to formally model data transformations, attacker assumptions, and system interactions. By composing de-identification transformations with re-identification relations, I verify whether privacy leakage is logically reachable.

Working thesis direction:
Relational Verification of Identity Disclosure in Data and AI Systems

Education

Ph.D. — Japan Advanced Institute of Science and Technology (JAIST)

Mar 2023 – Present · Expected Sep 2026 · Transdisciplinary Sciences / Information Science

M.S. — Japan Advanced Institute of Science and Technology (JAIST)

Apr 2020 – Feb 2023 · Transdisciplinary Sciences / Information Science

M.Div. — Biola University

Jun 2012 – May 2018 · La Mirada, California, USA · Intercultural Studies

Selected Publications

Relational Verification of Identity Disclosure Using Alloy

ABZ 2026 — International Conference on Rigorous State-Based Methods (Springer LNCS)

Formal Analysis of Re-identification Risks in Healthcare Data

Planned submission to Journal of Information Security and Applications (JISA)

Contact

Email: s2360003@jaist.ac.jp

I am interested in postdoctoral opportunities in formal methods, privacy, AI security, and LLM/RAG systems.

Advisor / Lab

Prof. Toshiaki Aoki
Aoki Laboratory (Formal Methods)
JAIST Aoki Lab

Ph.D. Candidate at JAIST

양승일

데이터 및 AI 시스템에서의 프라이버시와 개인정보 유출에 대한 형식 검증

저는 관계 논리, 모델 체킹, 그리고 시스템 수준 추론을 바탕으로 개인정보 유출과 재식별 위험을 배포 이전 단계에서 모델링하고 설명하며 검증하는 연구하고 있습니다.

현재의 연구는 개인 식별 노출을 관계적 도달 가능성 문제로 형식화하고, 이를 LLM 및 RAG 시스템까지 확장하는 데 초점을 두고 있습니다.

형식기법 프라이버시 & 보안 LLM / RAG 시스템 모델 체킹

논문 보기 연락하기 CV 다운로드

소개

저는 JAIST 융합과학 박사과정에 재학 중이며, 데이터 및 AI 시스템에서 발생하는 개인정보 유출, 재식별 위험, 프라이버시 침해 가능성을 형식적으로 모델링하고 검증하는 연구를 진행하고 있습니다.

특정 데이터 공개, 비식별화 정책, 또는 시스템 동작이 논리적으로 개인정보 유출로 이어질 수 있는지를 분석하는 검증 프레임워크를 개발하고 있으며, 경험적 프라이버시 평가와 형식적 보증을 연결하는 것을 목표로 하고 있습니다.

연구 초점

프라이버시 검증

설계 단계에서 개인정보 유출과 재식별 위험을 형식적으로 분석합니다.

관계적 도달 가능성

변환과 공격자 추론을 통한 도달 가능성으로 프라이버시 누출을 모델링합니다.

의료 데이터

민감한 의료 데이터와 구조화된 데이터 환경에서의 재식별 위험을 분석합니다.

LLM / RAG 보안

검색, 생성, 메모리, 문맥 기반 누출까지 형식적 프라이버시 분석을 확장합니다.

연구 관심

제 연구는 데이터 기반 시스템에서의 프라이버시와 보안을 위한 형식적 토대를 확립하는 것을 목표로 하고 있습니다. 개인정보 유출을 관계적 도달 가능성 문제로 모델링하며, 프라이버시가 안전한 상태를 데이터 변환과 추론 과정을 통해 식별 가능한 상태에 도달할 수 없는 상태라고 정의합니다.

이러한 관점은 설계 단계에서 프라이버시 위험을 검증할 수 있게 해 주며, 단순한 경험적 또는 통계적 접근이 아닌 논리적은 검증으로 증명 가능하게 합니다. 특히 LLM 및 RAG 시스템에서 형식 검증과 프라이버시 벤치마크, 감사 체계를 연결하는 데 관심을 가지고 있습니다.

방법론

저는 Alloy와 관계 논리를 사용하여 데이터 변환, 공격자 가정, 시스템 상호작용을 형식적으로 모델링합니다. 비식별화 변환과 재식별 관계를 결합하여 개인정보 유출이 논리적으로 도달 가능한지를 검증합니다.

박사논문 방향:
데이터 및 AI 시스템에서의 개인정보 유출에 대한 관계적 검증

학력

Ph.D. — Japan Advanced Institute of Science and Technology (JAIST)

2023년 3월 – 현재 · 2026년 9월 졸업 예정 · Transdisciplinary Sciences / Information Science

M.S. — Japan Advanced Institute of Science and Technology (JAIST)

2020년 4월 – 2023년 2월 · Transdisciplinary Sciences / Information Science

M.Div. — Biola University

2012년 6월 – 2018년 5월 · La Mirada, California, USA · Intercultural Studies

주요 논문

Relational Verification of Identity Disclosure Using Alloy

ABZ 2026 — International Conference on Rigorous State-Based Methods (Springer LNCS)

Formal Analysis of Re-identification Risks in Healthcare Data

Journal of Information Security and Applications (JISA) 투고 예정

연락처

이메일: s2360003@jaist.ac.jp

형식기법, 프라이버시, AI 보안, LLM / RAG 시스템 관련 포닥 기회를 찾고 있습니다.

지도교수 / 연구실

아오키 토시아키 교수
Aoki Laboratory (Formal Methods)
JAIST Aoki Lab

Ph.D. Candidate at JAIST

ヤン・スンイル

データおよびAIシステムにおけるプライバシーと個人情報漏えいの形式的検証

本研究では、関係論理、モデル検査、およびシステムレベルの推論を用いて、個人情報漏えいおよび再識別リスクをシステム導入前にモデル化・説明・検証します。

現在の研究は、アイデンティティ開示を関係的到達可能性問題として定式化し、これをLLMおよびRAGシステムへ拡張することを目的としています。

形式手法プライバシー・セキュリティ LLM / RAG システムモデル検査

論文を見る連絡する CV ダウンロード

概要

私はJAISTの融合科学分野に所属する博士課程学生であり、データおよびAIシステムにおける個人情報漏えい、再識別リスク、およびプライバシー問題を形式的にモデル化・検証する研究を行っています。

データ公開や非識別化ポリシーが論理的に個人情報漏えいへとつながるかどうかを分析する検証フレームワークを開発し、経験的評価と形式的保証を統合することを目指しています。

研究分野

プライバシー検証

設計段階で漏えいおよび再識別リスクを形式的に分析します。

関係的到達可能性

変換と攻撃者推論による到達可能性としてプライバシー漏えいをモデル化します。

医療データ

高感度データ環境における再識別リスクを分析します。

LLM / RAG セキュリティ

検索・生成・文脈による漏えい問題へ拡張します。

研究関心

本研究は、データ駆動型システムにおけるプライバシーとセキュリティのための形式的基盤の構築を目的としています。個人情報漏えいを関係的到達可能性問題として定式化し、識別可能状態に到達できないことをプライバシーとして定義します。

この枠組みにより、設計段階での厳密な検証が可能となり、従来の統計的手法を補完する理論的基盤を提供します。特にLLMおよびRAGシステムにおけるプライバシー検証とベンチマークへの応用に関心があります。

方法論

Alloyと関係論理を用いてデータ変換、攻撃者モデル、およびシステム相互作用を形式的に記述します。非識別化変換と再識別関係を組み合わせることで、漏えいの到達可能性を検証します。

博士研究テーマ：
データおよびAIシステムにおける個人情報漏えいの関係的検証

学歴

Ph.D. — Japan Advanced Institute of Science and Technology (JAIST)

2023年3月 – 現在 · 2026年9月修了予定

M.S. — Japan Advanced Institute of Science and Technology (JAIST)

2020年4月 – 2023年2月

M.Div. — Biola University

2012年6月 – 2018年5月

主な論文

Relational Verification of Identity Disclosure Using Alloy

ABZ 2026（Springer LNCS）

Formal Analysis of Re-identification Risks in Healthcare Data

JISA 投稿予定

連絡先

メール: s2360003@jaist.ac.jp

形式手法、プライバシー、AIセキュリティ、LLM / RAGに関するポスドクの機会に関心を持っています。

指導教員 / 研究室

青木　利晃（AOKI, Toshiaki）
Aoki Laboratory (Formal Methods)
JAIST Aoki Lab