Project summary

I am seeking $2,500 to present my accepted IWSEC 2026 paper, “Residual Execution Contracts for Compositional Security in Agentic Cyber-Physical Systems” and use the Tokyo visit for focused technical review with researchers working on formal methods and AI security. The research studies a compositional security problem in tool-using agents. Individual actions satisfy local admission conditions, followed by trajectories that cross a security boundary defined over execution history. Residual Execution Contracts maintain trusted execution state so later actions are evaluated in relation to security commitments established by earlier execution. The research has progressed through formal analysis and extensive empirical evaluation. The bounded residualization study evaluates 375k+ extensions and records matching decisions between the residual implementation and the full-trace reference monitor across the full evaluated set. The expanded adversarial evaluation covers 715,307 traces containing 80k+ raw-semantic hazards with REC preserving the declared contract across the evaluated traces. Concurrency receives a separate exact evaluation through 6,000 partially ordered batches. An independently implemented raw-semantic oracle agrees with the REC classifier across the full evaluated set and every certified schedule satisfies the modeled security contract under the declared execution assumptions. The definitive hosted evaluation studies 90 REC episodes for each of two model labels. REC preserves the declared endpoint constraints across every episode in both arms whereas interactive single-step mediation reaches unsafe endpoints in 52 of 90 episodes for one model and 48 of 90 for the second. These claims apply to the declared finite models under deterministic atomic-event semantics and complete modeled security state. The next research stage focuses on specification completeness as well as external technical evaluation. IWSEC is a great review setting for that transition bringing together researchers working on formal security analysis and cyber-physical security. I am also pursuing focused research meetings with groups at NII, NICT CREATE and Waseda.

What are this project's goals? How will you achieve them?

The trip will use the research results as the basis for external technical evaluation. The IWSEC presentation will expose the mechanism to researchers grounded in security enforcement and formal analysis with discussion focused on the assumptions governing specification completeness and modeled execution state. The Tokyo research meetings will extend that review through direct technical discussions on formal execution contracts and agent security. The strongest criticism from these interactions will feed into a follow-up evaluation program focused on adversarial specification gaps and richer execution environments. Within 30 days of IWSEC, I will publish a technical postmortem connecting the most substantive external criticism to specific experiments and formal research questions.

How will this funding be used?

The $2,500 goal supports a focused research trip centered on IWSEC 2026. Conference registration accounts for approximately $541 of the request and economy travel between the San Francisco Bay Area and Tokyo is budgeted at up to $1,250. Five nights of economical accommodation account for up to $500 with local transportation budgeted at up to $125. The remaining $84 covers necessary travel expenses.

Who is on your team? What's your track record on similar projects?

I am a research scientist trying to push the research agenda of formal verification for agentic systems. This project extends the ACM SaT-CPS 2026 paper, “Securing the Last Mile of CPS Control with Typed-Plan Firewalls,” published in the Proceedings of the 6th ACM Workshop on Secure and Trustworthy Cyber-Physical Systems. That earlier work studies typed admission checks for individual AI-generated actions. The IWSEC paper advances the research toward trajectory-level compositional security through Residual Execution Contracts and adds formal treatment of sequential execution together with concurrent action structures. Public supporting infrastructure includes LabTrust-Gym and the Open Verification Kernel.

What are the most likely causes and outcomes if this project fails?

The principal risk is limited technical yield from the external review.

How much money have you raised in the last 12 months, and from where?

I am pursuing partial research-visit support from Japanese host institutions.