Lier une entrée cachée à un comportement natif.
Une ligne de recherche en attestation RISC-V qui relie une entrée externe privée à une exécution native authentifiée dans un modèle de moniteur déclaré.
- Publié
- Mis à jour
Périmètre du projet
ACTUEL / RECHERCHE
Protocol and verification design
- Closed foundation
- Phase 1R.3B execution-input binding
- Recorded evidence
- 17/17 canonical sessions and 73/73 adversarial cases in the declared scope
- Execution model
- Trusted sensing/authentication software-QEMU monitor
Thèmes
The hidden-input problem
A verifier may need confidence that a native program consumed a genuine external input and that the input caused the machine behaviour being attested, while the input and sensitive intermediate state remain private.
That is more specific than proving that a program has some valid execution. The chain must connect origin, consumption, program-derived state, authenticated behaviour and verifier policy.
Prove one narrow connection first
The Phase 1R.3B foundation closes a narrower subproblem: binding a selective zero-knowledge branch witness to the scalar actually observed at an authenticated RISC-V function entry. Its recorded canonical and adversarial sessions belong to that scope.
The result is useful because it identifies what the proof must bind at the execution boundary; it is not a shortcut to a claim about every native program or every monitor.
Privacy is part of the evidence model
A successful proof is not enough if the evidence files leak the protected input, hidden registers or blinding values. The system therefore treats privacy audit, session custody, challenge freshness and public leakage as explicit properties.
This makes the verifier's view part of the protocol design instead of an afterthought added after the cryptographic relation is written.
The next phase remains a hypothesis
The planned direction is private causal native-execution attestation: connect authenticated input provenance to a conservative data-dependence slice and then to verifier-interpreted machine behaviour without re-proving an entire native execution in a generic zero-knowledge VM.
That is a research hypothesis with open novelty, security and execution obligations. The page records the foundation and its limits rather than presenting the future chain as finished.
Limite de l'évidence publique
The completed foundation is bounded to its declared monitor and software-QEMU model. Phase 2 is a research direction, not a completed security result; arbitrary-program support, malicious-monitor resistance, hostile-kernel erasure, compiler correctness and universal performance remain unclaimed.
Ces pages publient un périmètre d'ingénierie et un raisonnement vérifiables ; les preuves de projet sont ajoutées lorsqu'elles sont prêtes à être partagées.
Voir tous les projets d'ingénierie