The purpose of this e-mail is to start a discussion/debate around the issue that I raised in the tech-chairs meeting this week related the m-mode and the stability of the configuration.  It is important to state that there is nothing that I am discussing in the e-mail that would be considered confidential by my corporation.

As most of you will be realize I am relatively new to the RISC-V community since I started my participation earlier this year. I read the privilege specification and probably need to reread it. MY concern comes from my focus as a security researcher. Specifically, I am working on confidential computing.  My current focus included what I will call provable security. Some might call this “certifiable security”, referring to the various methods to certify the security strength of an apparatus. For the highest levels of certification, in general, a proof (mathematical) of the attributes of the system is required.  In this model, trust is not a replacement for proof. Just because something is trusted, does not mean that its attributes do not have to be verifiable (or proven). I apologize if I am expressing a concern that does not exist because I am still learning the architecture.

I did not do a good job of describing the concern in the tech chairs meeting.  I will try to be less expressive and clearer in this e-mail.  I have two areas of concern 1) attestation and 2) Proof.

Attestation is the notation that the configuration of a system can be confirmed by an external party (assuming the underlying system meets certain requirements). For confidential computing, the attestation must include information about the control status registers (CSRs) (hardware configuration).  Some, but not all, of the hardware configurations must be part of the attestation. It does not matter who owns the CSR if the attested value cannot change without a reset of the system. This requirement for confidential computing is reflected in TCG DICE in that notification is required if the configuration of a dedicated device is modified.  If this is not true, then the attestation is of little value because the remote party will not know whether the values represent the current configuration of the system.  If it existed,  “dynamic attestation” does not solve the problem because the remote party would not know for how long the values were accurate. Dynamic attestation can have value but not in this space.  The key phrase in my earlier statement is “but not all”. In my opinion this implies a requirement that those CSRs that affect the security of the system, or the security of confidential computing must be lockable. The lock must be verifiable and not changeable without rebooting the system. Simply put confidential computing requires that these registers can be locked, and their lock state is verifiable. Obviously if M-mode owns the CSR, then it would have to properly configure the CSR before locking (and measuring) it. This is not a requirement that it be locked in all versions of RISC-V, or M-mode firmware, etc. just those that support confidential computing.  This is work that AP-TEE group (and any other group implanting CC support for a variant of RISC-V) must do. In terms of implementation rather than the overkill of a global bit which freezes all CSRs, I prefer that those registers which are a concern should have a bit indicating that they have been locked or perhaps a locking register indicating that certain sets of registers have been locked.

Proof is a bit more complex. Addressing the issue at a high level, fundamentally hardware and software are both Touring complete.  This means that theoretically we can prove the attributes of the hardware (often called verification) and we can prove the attributes of software.  The more complex the hardware or software is, the more difficult a formal proof is. Obviously the more complex the hardware or software is, the more difficult is to prove its attributes. In general, for automated mathematical proofs of software one must also prove that the mathematical expression represents the actual coded unless there is an automated tool for deriving the expressions from the code. (a longer discussion). Some languages are easier to prove than others. However, for the work we are doing (bias warning) we need to establish invariants for our system and our mathematical proofs will verify or confirm that the invariants are not broken by the code. Since we are not yet focused on proving the hardware our invariants describe the environment provided by the hardware. The things that our proofs are based on should not (cannot) be mutable without hardware reset. Since we are focused on confidential computing, solving the issue for attestation should address our concerns.

I personally believe that attributes of the RISC-V architecture provide a better foundation for the types of work we are doing. If possible, it would be good to have proofs.