Researcher in Systems Security & Applied Cryptography
Department of Computer Science & Systems, Hanyang University • Seoul, South Korea
Laboratory for High-Assurance Systems & Foundations of Verifiable Computation

Official Portal • GitHub Profile • GitLab Research Mirror • Institutional Inquiries

Support Independent Research
I am an independent researcher engineering open-source systems security tools, applied cryptographic primitives, microhypervisors, and verifiable computing primitives. All research across these repositories is self-directed and personally funded. Any monetary support, institutional research grants, or individual sponsorship to help fund server compute, test hardware, publication costs, and ongoing development is deeply appreciated.

             [ Formal Verifiability & Mathematical Rigor ]
                                  |
    +-----------------------------+-----------------------------+
    |                             |                             |
[ Hardware Virtualization ]  [ Verifiable Proofs ]  [ Program De-virtualization ]
    - Microhypervisors           - IVC & Folding        - SMT Symbolic Execution
    - EPT / VMCS Proofs          - SP1 zkVM Harnesses   - LLVM IR Semantic Recovery

My research operates at the nexus of hardware-assisted systems virtualization, verifiable computation (Zero-Knowledge Proofs & Incrementally Verifiable Computation), and automated binary analysis/compiler security. The overarching objective is to establish provable execution guarantees for untrusted virtualized environments while engineering deterministic mathematical frameworks for de-obfuscating protected native software.

• Hardware-Assisted Virtualization & Microhypervisors: Formal verification of Extended Page Table (EPT) state transitions, Virtual Machine Control Structure (VMCS) invariant enforcement, and zero-trust nested virtualization primitives on bare-metal x86_64 and RISC-V architectures.
• Incrementally Verifiable Computation (IVC) & Folding Schemes: Lookup-accelerated folding architectures (Nova, SuperNova, and HyperNova paradigms) applied to hypervisor transitions, zkVM verification harnesses, and trustless state transitions.
• Binary De-virtualization & Program Synthesis: Abstract interpretation, SMT-driven symbolic execution (Z3), control flow graph (CFG) normalization, and intermediate representation (LLVM IR) lifting targeting multi-layered commercial virtualization-based obfuscators.
• Post-Quantum Cryptography & High-Assurance Runtimes: Lattice-based Fully Homomorphic Encryption (BFV/CKKS) for privacy-preserving computation, zero-retention compliance engines, and deterministic monorepo verification pipelines.
• Deterministic Edge & Mobile Agent Architectures: Mathematical pacing models for personal productivity, discrete goal decomposition algorithms, and finite-state persona synthesis engines (mobile-butler).

Quantitative breakdown of active open-source systems, experimental compilers, and research codebases:

Verifiable Hardware-Assisted Virtualization via Lookup-Accelerated Incremental Folding over Extended Page Tables and VMCS Transitions

• Introduces an Incrementally Verifiable Computation (IVC) architecture for proving correct hardware virtualization state transitions without trusting the host hypervisor.
• Encodes 4-level x86_64 EPT paging structures and VM-exit/VM-entry VMCS register states into committed polynomial relations.
• Combines log-derivative multiset lookup arguments with SP1 RISC-V zero-knowledge verifiable execution harnesses.
• Evaluated across 43 automated formal test suites with multi-OS verification pipelines.

Also home to wasm-superopt, a WebAssembly deobfuscator built on simplifications that are proofs, and absint, an abstract interpretation analyzer for memory safety and data races. Automated Symbolic De-virtualization & Intermediate Representation Lifting Engine

• Research framework targeting layered virtualization-based commercial obfuscators (VMProtect).
• Employs dynamic trace recording, taint analysis, dead-code elimination, and symbolic simplification via Z3 SMT solver.
• Recovers normalized Control Flow Graphs (CFGs) and re-synthesizes optimized LLVM IR from obfuscated bytecode interpreter loops.

Its core cryptography is also one WebAssembly Component with no imports, running unchanged from Python, TypeScript and Go. Lattice-Based Post-Quantum Medical Data Cryptography & FHE Suite

• Implements ring learning with errors (RLWE) Fully Homomorphic Encryption schemes (BFV and CKKS) for blind diagnostic evaluation.
• Features multi-party secret sharing, verifiable zero-knowledge clinical inference, and post-quantum digital signatures.
• Verified with strict documentation assertions, zero-warning rustdoc builds, and automated security audits.

Deterministic, Zero-Retention Enterprise Policy & Compliance Auditing Suite

• Monorepo matrix impact analysis engine utilizing Wilson score dampening to prune unimpacted CI test cells.
• Pre-flight DDL lock-hazard AST detector for PostgreSQL migrations (Prisma, Flyway, Alembic) and schema drift verifier.
• Zero-retention PII scanner supporting direct PDF content stream rewriting and dual pure-JS/WASI-Go WebAssembly kernels.
• Complete deterministic test coverage across 90 unit and dist-equivalence verification suites.

All-in-One Ethereum Toolchain, Visual Forensics & Smart Contract Security Hub

• Unifies smart contract compilation, formal SMT verification, stateful dynamic fuzzing, storage collision diffing, and live REPL scratchpad into a single native binary (para).
• Features a Chainalysis Reactor-grade on-chain visual forensics kit with multi-hop fund flow tracing, OFAC SDN sanctions screening, direct mixer taint calculation, and automated compliance dossier generation.
• Features complete user-centric onboarding documentation, quickstart workflows, and safety FAQs in the Dedicated Wiki.

Ultra-Fast, Memory-Safe Carbon Language Compiler, SemIR Engine & REPL

• High-performance, zero-dependency Carbonation toolchain written in 100% safe Rust with zero segfaults or memory leaks.
• Features complete end-to-end SemIR (Semantic IR) pipeline, direct C99/C++ translation, native -O3 assembly code generation, and interactive REPL.
• Built-in bytecode re-virtualizer and Control Flow Flattening (CFF) runner for code protection.

Bare-Metal Sovereign Microkernel & Hypervisor Research Systems

• aether: Minimalist x86_64 hardware hypervisor enforcing capability-based memory isolation and strict hypercall interfaces.
• holynix: 64-bit ring-0 operating system kernel written in HolyC with pure C fallback support, custom memory allocators, and multitasking scheduler.

Peer-Reviewed Research Implementations & Reproducibility Packages

• Official artifacts accompanying peer-reviewed journal/conference submissions.
• Contains end-to-end evaluation scripts, raw benchmark telemetry, and automated verification suites.

A replicated micro-VM cluster built from scratch: Raft consensus with pre-vote and check-quorum, a KVM and Hypervisor.framework micro-VM manager that boots a real Linux kernel, and a Cranelift JIT with gas metering, differentially tested against a reference interpreter.

Conway's Game of Life with bit-sliced and Hashlife engines, and a falling sand world with regions that sleep when nothing in them moves.

A zero-boxing bytecode VM and a Brainfuck compiler that emit JVM bytecode into hidden classes, so the JVM's own JIT turns them into native code.

A KSP2 processor that generates zero-reflection, zero-allocation bitmask diffs and struct mappers at compile time, with incremental builds.

A BitTorrent client and Kademlia DHT node in Kotlin coroutines, with magnet links, request pipelining and iterative lookups.

A transit app for all of Korea in Kotlin Multiplatform, for Android, iOS and the web: platform boards with sound and moving trains, network maps generated from open data, offline trip planning, walking and driving directions on a vector map it draws itself, and routes abroad.

Multi-engine reverse-engineering platform (v7.0.1) combining a 16-crate native Rust workspace (Mach-O, ELF, PE, DEX, WebAssembly, and archive parsers; x86/x86_64/ARM/AArch64/sBPF decoders; CFG and dataflow recovery; clean-room Pseudo-C decompiler; hash-chained evidence ledger; egui desktop workbench) with a 302-tool Model Context Protocol (MCP) server.

Cross-checks what Korean listed companies report in their financial statements against independent audit reports, OpenDART XBRL, US SEC 20-F filings, credit ratings, and public registries across 10 verification layers, evaluated under a pre-registered 39-company-year validation protocol.

1. zk-HyperKVM: Verifiable Hardware-Assisted Virtualization via Lookup-Accelerated Incremental Folding over Extended Page Tables and VMCS Transitions
   Jeong Hoon Kim
   Cryptology ePrint Archive / Research Monograph, 2026.

2. TACC: Trustworthy Access Control and Collaborative Framework for Decentralized Compute
   Jeffrey Kim, et al.
   Elsevier Publications / Research Proceedings, 2026.

3. Educhain: Verifiable Academic Credential Ledger with Zero-Knowledge Selective Disclosure
   Jeffrey Kim, et al.
   Elsevier Publications / Research Proceedings, 2026.

4. Monograph I: A Treatise on Epistemic Justification Beyond Cognitive Surveyability in Automated Proof Verification
   Jeong Hoon Kim
   Theoretical Computer Science & Mathematical Foundations Monograph, 2026.

All maintained repositories conform to strict safety and continuous verification standards:

• Zero-Warning Compilation Policy: Built with RUSTFLAGS="-D warnings" (Rust) and strict compiler flags (-Wall -Wextra -Werror in C/C++).
• Multi-Platform Verification Matrix: Automated CI validation runs across ubuntu-latest and macos-latest runners on every commit.
• Automated Security Auditing: Scheduled dependency vulnerability scans (cargo audit, npm audit) and automated secret leak prevention (gitleaks).
• Cryptographic Reproducibility: Pinned toolchains, deterministic builds, and standalone verification vectors.

As an individual student researcher working without external venture capital or dedicated corporate grants, all research prototypes, formal verification harnesses, and high-assurance compiler toolchains are built independently.

Financial contributions directly sustain:

• Cloud compute infrastructure and CI runner minutes for extensive test matrix suites.
• Dedicated hardware testbeds for bare-metal x86_64 and RISC-V virtualization research.
• Independent academic publication costs and monograph dissemination.

For protocol contributors and researchers who prefer direct on-chain settlement:

For dedicated on-chain payment hashes or invoice receipts, please email jk9576@hanyang.ac.kr.

In addition to academic research, I accept high-leverage technical consulting engagements, protocol security audits, and private advisory for engineering teams:

To request a private scoping call, advisory retainer, or fixed-rate quote for an audit:

• Email: jk9576@hanyang.ac.kr (include project scope, timeline, and code repository links).
• Turnaround: Initial scope review and feasibility response within 24 hours.

• Institutional Affiliation: Department of Computer Science & Systems, Hanyang University, Seoul, South Korea
• Institutional Email: jk9576@hanyang.ac.kr
• GitLab Research Mirror: gitlab.com/jk9576
• GitHub Repository: github.com/Aetherx86
• Cryptographic Authentication: Public key fingerprints and signed commits available upon authenticated request.