Closed muhammad-usama-sardar closed 1 year ago
Thanks very much Usama.
I support this effort, however I'd like to get a couple of clarifications.
First item:
Design of attestation architecture for Confidential Computing including coding part (formal specification and analysis of all phases of attestation mechanisms in ProVerif and other suitable formal tools and techniques)
I thought the goal was to provide formal analysis of existing attestation architectures. The phrasing though is slightly confusing: it reads like you want to "design an attestation architecture for CC"?
Second item, it is not clear to me what you mean by:
[...] including coding part (representation in generic formalism)
First item:
I thought the goal was to provide formal analysis of existing attestation architectures. The phrasing though is slightly confusing: it reads like you want to "design an attestation architecture for CC"?
Indeed formal analysis of existing attestation architectures is one of the sub-goals. We will provide all support for attestation in CCC projects as well as others. But I would like to aim one step ahead, i.e., to have formal definitions and semantics associated with the attestation mechanisms, and then instantiate all existing ones in one of the three categories. In short, the design is from formal perspective.
Second item, it is not clear to me what you mean by:
[...] including coding part (representation in generic formalism)
Each Claim and each category will have formal definitions and semantics associated with it. For example, we will precisely define what exactly is meant by runtime measurement as a Claim.
First item: I thought the goal was to provide formal analysis of existing attestation architectures. The phrasing though is slightly confusing: it reads like you want to "design an attestation architecture for CC"?
Indeed formal analysis of existing attestation architectures is one of the sub-goals. We will provide all support for attestation in CCC projects as well as others. But I would like to aim one step ahead, i.e., to have formal definitions and semantics associated with the attestation mechanisms, and then instantiate all existing ones in one of the three categories. In short, the design is from formal perspective.
This looks to me like a very broad and long term ambition rather than a goal that can be achieved in a finite amount of time with limited resources. My suggestion would be to break it down into a set of incremental sub-goals that are logical steps for achieving your objective on which we can then decide priorities, assignees, etc. Scoping this project becomes very hard / impossible otherwise.
Another suggestion I have is to split these two points into separate project proposals. Whilst they can obviously feed into each other, they are also sufficiently orthogonal to deserve independent life.
Second item, it is not clear to me what you mean by:
[...] including coding part (representation in generic formalism)
Each Claim and each category will have formal definitions and semantics associated with it. For example, we will precisely define what exactly is meant by runtime measurement as a Claim.
OK, thanks. This goal is clear to me now. I suggest you edit the proposal with this explanation.
This looks to me like a very broad and long term ambition rather than a goal
Updated. Please have a look.
I suggest you edit the proposal with this explanation.
Done
This looks to me like a very broad and long term ambition rather than a goal
Updated. Please have a look.
Thanks Usama!
One nit, when you say: "Refinements of standard attestation architecture and precisely define terminology for Confidential Computing" you mean "[...] terminology for attestation in Confidential Computing", right?
Note that in TAC we worked on a "Common Terminology for Confidential Computing" document.
One nit, when you say: "Refinements of standard attestation architecture and precisely define terminology for Confidential Computing" you mean "[...] terminology for attestation in Confidential Computing", right?
Thanks for the catch. Yes, I intended only for attestation. Clarified.
@KeithMoyer @MikeCamel @gkostal @thomas-fossati @shnwc Based on the discussions in last meeting, I have limited the scope of the project, and added potential outcomes as well as conformance with the charter. Please leave your comments/issues/concerns/questions latest until 24.02.
Categorization of solutions into 3 major groups (vendor solutions, architecture lead solutions, and frameworks)
This seems unnecessarily prescriptive. Perhaps "categorize existing attestation-related products into high-level types, based on their role in the ecosystem"?
Reduce the increasing terminology hell generated by each vendor and framework
Unnecessarily inflammatory wording, and has no measurable outcome.
Facilitate the end users in making a suitable choice
A choice of what? What's suitable? What's the actual output of this effort related to this?
Provide strong formal guarantees for attestation to facilitate wider adoption
I think this needs more clarification, based on our discussion in the last meeting. Perhaps something like the following? "Create formal models describing generic attestation protocols and proving their security properties, based on assumed properties of the underlying technology. (as a second, potentially stretch goal) Create a mapping of existing confidential computing technologies to the properties assumed in the generic model."
Updated the issue. Here is a short summary:
Categorization of solutions into 3 major groups (vendor solutions, architecture lead solutions, and frameworks)
This seems unnecessarily prescriptive. Perhaps "categorize existing attestation-related products into high-level types, based on their role in the ecosystem"?
Agree. The scope of proposal is "attestation in confidential computing". So it implicitly applies to everything. I stated it explicitly now.
Reduce the increasing terminology hell generated by each vendor and framework
Unnecessarily inflammatory wording, and has no measurable outcome.
This "inflammatory wording" was coined by your colleague Razieh Behjati during her invited talk at PAVeTrust, and I can't agree more with this. For example, having "Verifier" instead of the fancy naming "steward" on slide 14 of a recent CCC SIG talk of Dmitri would have been much more understandable.
Facilitate the end users in making a suitable choice
A choice of what?
choice of:
What's suitable?
suitable meaning an informed decision for the use-case at hand
What's the actual output of this effort related to this?
Actual output is a comparison of tradeoffs and understanding of assumptions for each considered product
Provide strong formal guarantees for attestation to facilitate wider adoption
I think this needs more clarification, based on our discussion in the last meeting. Perhaps something like the following? "Create formal models describing generic attestation protocols
"Create formal models describing generic attestation protocols" is already captured by "formal specification" in the proposal.
and proving their security properties,
This is already captured by "formal analysis" in the proposal.
based on assumed properties of the underlying technology.
This is an outcome of the effort, i.e., understanding the trust assumptions required to prove the properties.
(as a second, potentially stretch goal) Create a mapping of existing confidential computing technologies to the properties assumed in the generic model."
This is already captured by "Instantiation of 2 prominent solutions in each group". We have formal specifications of Intel SGX, Intel TDX, Arm CCA, and SCONE already (here).
As far as I can tell from reading this proposal, it's proposing a project to formally specify and analyze all protocols used in remote attestation scenarios for all commercially available TEE technologies. The results, surprisingly to me, aren't to reach conclusions about the security characteristics of the protocols -- but to improve terminology, identify ambiguities/contradictions, and create building blocks.
The scope appears huge and open-ended. There are numerous commercial technologies -- and quite possibly will grow at a rate that can't be kept up with in the formal analysis. Terminology always evolves. Building blocks can always be improved or address different requirements.
Some of the proposed deliverables don't appear to align with the "contribute to open source solutions" charter of the group. The analysis and specifications seem like they could align -- but feedback to various parties on terminology/ambiguities/contradictions doesn't.
In a nutshell, I'd suggest moving most of the current text into a background document which provides context and aspirational goals. Then I'd suggest creating a scoped list of a few goals achievable in six months to work on first -- described as specific deliverables (e.g. ProVerif specification for Versaison attestation protocol XXX, along with analysis determining security characteristics).
As far as I can tell from reading this proposal, it's proposing a project to formally specify and analyze all protocols used in remote attestation scenarios for all commercially available TEE technologies.
The proposal claims to cover only two prominent solutions in each group. We never claimed to cover all. We aim to be general enough that others can be mapped in similar way but covering all is not the aim.
In a meeting with the chairs on 01.03, we unanimously agreed to pursue the sub-project as described in the issue, and consider the remaining goals (e.g., generic formalisms and interoperability) as a future sub-project.
@thomas-fossati please create a repo preferably with the name formal-spec-TEE
under the SIG, and add it to sub-projects here. You may close the issue once done.
@thomas-fossati please create a repo preferably with the name
formal-spec-TEE
under the SIG, and add it to sub-projects here. You may close the issue once done.
Done. Closing.
I think we might have jumped the gun here on closing the issue and creating a repo. From a process standpoint, I'd like that if we take a vote, we do so in the regular bi-weekly meeting or over the mail list for full transparency. My sense from discussing this with some of the people present in the breakout meeting is that there was not necessarily unanimous agreement in the sense of approving the project as written, but perhaps some loose agreement about how changes to the scope were verbally provided. As it is currently written the scope is unclear to me. Attestation itself is not a protocol and all of the scope then defined on the formal verification of a protocol does not make sense to me. I would appreciate if this issue were re-openned; the scope clarified; then a public vote taken whether or to proceed, once the scope is clarified.
I think we might have jumped the gun here on closing the issue and creating a repo. From a process standpoint, I'd like that if we take a vote, we do so in the regular bi-weekly meeting or over the mail list for full transparency. My sense from discussing this with some of the people present in the breakout meeting is that there was not necessarily unanimous agreement in the sense of approving the project as written, but perhaps some loose agreement about how changes to the scope were verbally provided.
A rough consensus was already developed in the Feb meeting where the group agreed that formal verification is a vital activity and of tremendous value. The only leftover scoping was managed in a focused meeting. We closed the focused meeting with a full consensus on limiting the scope as defined. For full transparency, can you put in the names of the people you discussed with and who seem not to have agreed to this? Why did they not raise this concern themselves?
As it is currently written the scope is unclear to me. Attestation itself is not a protocol and all of the scope then defined on the formal verification of a protocol does not make sense to me.
What is your definition of the protocol?
I would appreciate if this issue were re-openned; the scope clarified; then a public vote taken whether or to proceed, once the scope is clarified.
I wouldn't mind re-opening, but for transparency I would like you to bring in a genuine reason/critique to reopen this. This includes the chairs in the breakout meeting pasting their concerns here.
A rough consensus was already developed in the Feb meeting where the group agreed that formal verification is a vital activity and of tremendous value. The only leftover scoping was managed in a focused meeting. We closed the focused meeting with a full consensus on limiting the scope as defined.
My understanding is different. In previous meetings, I did not vote either way since the proposal was not clear to me. In the focus meeting, my opinion was still to update the proposal, then we will have a chance to review and comment. So I was surprised when I saw the comments claiming full consensus and the repo opened overnight.
My understanding is different. In previous meetings, I did not vote either way since the proposal was not clear to me. In the focus meeting, my opinion was still to update the proposal, then we will have a chance to review and comment. So I was surprised when I saw the comments claiming full consensus and the repo opened overnight.
You never raised any concern in the several months of the discussion of the proposal so far. I am surprised that you have concerns all of a sudden.
Reopening as requested by @dcmiddle in https://github.com/CCC-Attestation/governance/issues/9#issuecomment-1467040405
For the record: I think Usama's proposal as currently described has well-defined scope and deliverables, and I am happy to make it a CCC attestation project.
For what it's worth, I am generally in agreement with the current proposal and would approve it in its current form¹. However, I was also surprised that it was considered closed and the project was created after the small meeting that we had. In the future, I think we can avoid this by being explicit when a "vote" is being done (as required by the non-technical charter https://github.com/CCC-Attestation/governance/blob/main/NON_TECHNICAL_CHARTER.md ):
Mechanisms for adding deliverables:
I interpreted the small meeting as having reached a "loose consensus", but not a "voting by chairs". Because I feel the voting should happen in the open (in a public SIG meeting, on the public mailing list, or perhaps only on a github issue if "public" comment isn't needed), I had expected the proposal to be cleaned up and ready for a vote in the next SIG meeting. If the feedback from the small meeting were incorporated into the proposal (which I feel it, by and large, was), the vote should have been an easy one (with, at most, some nits with contingent approval). The proposal had been discussed for a long time, and we just needed to get the consensus adequately captured in the proposal.
Thank you for your patience, Usama, as we iron out our governance procedures!
¹ I also wouldn't be opposed to some fine-tuning to add some specificity, as I think is being proposed by Dan. However, perhaps an option is to incorporate those details in the new project's README as long as we have confidence that we're not talking about different goals in the proposal (in keeping with the goal of "bias towards action" in the non-technical charter for this SIG).
On Thu, Mar 16, 2023 at 10:04 AM Thomas Fossati @.***> wrote:
For the record: I think Usama's proposal as currently described has well-defined scope and deliverables, and I am happy to make it a CCC attestation project.
— Reply to this email directly, view it on GitHub https://github.com/CCC-Attestation/governance/issues/9#issuecomment-1472365248, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAHXEE25TF5SQIWYPKBUNVTW4NBZRANCNFSM6AAAAAAUEDSVTY . You are receiving this because you were mentioned.Message ID: @.***>
--
Keith Moyer | Software Engineer | @.*** | 425-936-4301
My current thoughts:
However, I was also surprised that it was considered closed and the project was created after the small meeting that we had.
I interpreted the small meeting as having reached a "loose consensus", but not a "voting by chairs". Because I feel the voting should happen in the open (in a public SIG meeting, on the public mailing list, or perhaps only on a github issue if "public" comment isn't needed), I had expected the proposal to be cleaned up and ready for a vote in the next SIG meeting. If the feedback from the small meeting were incorporated into the proposal (which I feel it, by and large, was), the vote should have been an easy one (with, at most, some nits with contingent approval).
I think that was the very purpose of the small meeting. If the goal was to wait 2 weeks for a public vote, there was actually no need of this small meeting.
I also wouldn't be opposed to some fine-tuning to add some specificity, as I think is being proposed by Dan.
One has to come up with some genuine concerns which can be addressed.
as we iron out our governance procedures!
A simple question to you and other chairs: Why were these governance procedures not followed for Issue #8? Why was it closed abruptly saying
Since there is no objection from other chairs, I'll move forward to create the repo.
On the other hand, the topic doesn't appear to directly align with the non-technical charter (which focuses on interoperability along with authoring code).
We all agree that it aligns fully with §1b of Technical charter. Regarding non-technical charter, the original proposal did include interoperability with generic formalism which was removed on recommendation of chairs to limit the scope. Anyway, the currently scoped project can be thought of as foundational work for a future project and therefore, I don't see any hurdle in this.
- project definition - I would like to see the clause "and other suitable formal tools and techniques" clarified or eliminated.
eliminated
I'd also like to see the term "artifacts" replaced with specific deliverables. That said, I am OK with this further clarification captured in the project's README.MD file.
"artifacts" here are simply protocol specification in ProVerif spec language and property specification. With "and other suitable formal tools and techniques" removed, this should be obvious now.
Hi, my interest is not in what is and isn't a protocol. It is in trying to understand what scope you are proposing. TDX provides primitives that can be used to construct various protocols. Is there a specific protocol that you are seeking to formalize?
I am more confused by this reference:
We have formal specifications of Intel SGX, Intel TDX, Arm CCA, and SCONE already (here).
If you already have formal specifications for those products as part of your earlier work then is this proposal just adding AMD SEV-SNP?
Incidentally is this self-published or from ACM? It renders this in my PDF viewer: Muhammad Usama Sardar, Thomas Fossati, and Simon Frost. 2022. SoK: Attestation in Confidential Computing. In Proceedings of ACM Conference (Conference’17). ACM, New York, NY, USA, 17 pages. Conference’17, July 2017, Washington, DC, USA
I'd also like to see the term "artifacts" replaced with specific deliverables. That said, I am OK with this further clarification captured in the project's README.MD file.
"artifacts" here are simply protocol specification in ProVerif spec language and property specification. With "and other suitable formal tools and techniques" removed, this should be obvious now.
and
Hi, my interest is not in what is and isn't a protocol. It is in trying to understand what scope you are proposing. TDX provides primitives that can be used to construct various protocols. Is there a specific protocol that you are seeking to formalize?
I am more confused by this reference:
We have formal specifications of Intel SGX, Intel TDX, Arm CCA, and SCONE already (here).
If you already have formal specifications for those products as part of your earlier work then is this proposal just adding AMD SEV-SNP?
Please add clarification to the scope and the deliverables of the proposal.
Hi, my interest is not in what is and isn't a protocol. It is in trying to understand what scope you are proposing.
Thank you for clarifying.
TDX provides primitives that can be used to construct various protocols. Is there a specific protocol that you are seeking to formalize?
Here is where I would disagree. From a cryptographic perspective, attestation in TDX is itself a protocol as it has various roles (TD QE, TDX Module, TD, CPU etc.) and cryptographic operations (MAC, Signatures) involved. This protocol can be composed with other protocols (such as TLS or SPDM and vTPM attestation protocol) according to use case. The verification of the composition of RA and TLS protocols for Arm will be carried out as part of #7, and it is not in scope for this specific project.
I am more confused by this reference:
We have formal specifications of Intel SGX, Intel TDX, Arm CCA, and SCONE already (here).
This refers to previous work:
If you already have formal specifications for those products as part of your earlier work then is this proposal just adding AMD SEV-SNP?
Well, the original project scope back then was to add a 2nd TEE/framework in each category (vendors solutions, architecture lead solutions, and frameworks) and then generalize. The chairs decided to limit the scope to TDX, CCA and SEV-SNP only, and have the rest as a follow-up project for the future.
All the publicly available specs for attestation protocol in Arm CCA and Intel TDX have been modeled. I will be happy to extend it if Arm or Intel can share further details.
Incidentally is this self-published or from ACM? It renders this in my PDF viewer: Muhammad Usama Sardar, Thomas Fossati, and Simon Frost. 2022. SoK: Attestation in Confidential Computing. In Proceedings of ACM Conference (Conference’17). ACM, New York, NY, USA, 17 pages. Conference’17, July 2017, Washington, DC, USA
This is a pre-print, and the conference text shown there is the default text in the ACM LaTeX format.
Please add clarification to the scope and the deliverables of the proposal.
Done
I think that was the very purpose of the small meeting. If the goal was to wait 2 weeks for a public vote, there was actually no need of this small meeting.
It was needed because we had discussed the issue repeatedly, and the feedback given was not incorporated into the proposal in the way those giving that feedback expected. It seemed like there was miscommunication and a dedicated meeting to make sure everyone understood each other seemed warranted. I don't think anyone wanted another round of discussion in the SIG with the outcome of "please update the proposal to be more clear about the scope and outcomes" as had been said in the previous meetings.
One has to come up with some genuine concerns which can be addressed.
Please, let's remain civil. Suggesting that the concerns expressed are not genuine does not help ease those concerns.
A simple question to you and other chairs: Why were these governance procedures not followed for Issue #8? Why was it closed abruptly saying
Since there is no objection from other chairs, I'll move forward to create the repo.
I explicitly worded my I support creation of this project
comment with the intent of it acting as my vote. I wholeheartedly agree that procedures should have been followed more closely with the rest of the chairs doing the same.
I think that was the very purpose of the small meeting. If the goal was to wait 2 weeks for a public vote, there was actually no need of this small meeting.
It was needed because we had discussed the issue repeatedly, and the feedback given was not incorporated into the proposal in the way those giving that feedback expected. It seemed like there was miscommunication and a dedicated meeting to make sure everyone understood each other seemed warranted. I don't think anyone wanted another round of discussion in the SIG with the outcome of "please update the proposal to be more clear about the scope and outcomes" as had been said in the previous meetings.
Let's face it! There were multiple talks already on the topic by myself and Tom. In light of that, the scope and outcomes were very clear from the beginning. The scope was to add another instance (ideally a very different one to cover diversity) in all of the three categories (hardware vendors, architecture lead solutions and frameworks) and to compare and contrast in each category and attempt towards generalization and interoperability. Outcomes were proofs in ProVerif and generalizations. It was never the clarity of scope which was criticized. It was only the huge amount of work that was underneath the proposal. Scope, specially for research projects, is not a binary thing. Some things should intentionally be left out open to be filled as the research in the area matures.
One has to come up with some genuine concerns which can be addressed.
Please, let's remain civil. Suggesting that the concerns expressed are not genuine does not help ease those concerns.
I am not suggesting anything. I don't see any genuine concern which I could address.
A simple question to you and other chairs: Why were these governance procedures not followed for Issue #8? Why was it closed abruptly saying
Since there is no objection from other chairs, I'll move forward to create the repo.
I explicitly worded my
I support creation of this project
comment with the intent of it acting as my vote. I wholeheartedly agree that procedures should have been followed more closely with the rest of the chairs doing the same.
I am not referring to your vote. @gkostal and @MikeCamel as chairs have never commented on that issue and never voted publicly! Why was the issue closed without their public vote? Where is the full transparency thingy pointed out by Dan? Why is that issue not reopened for fairness?
It was never the clarity of scope which was criticized.
It is my recollection that this was actually the primary point of concern of the group (at least it was my primary concern)
I am not referring to your vote. @gkostal and @MikeCamel as chairs have never commented on that issue and never voted publicly! Why was the issue closed without their public vote? Where is the full transparency thingy pointed out by Dan? Why is that issue not reopened for fairness?
I want to reiterate that I do not feel that process was followed as exactly as it should have been in #8. Approval can be reasonably inferred from the comments of 3/5 chairs, but we should have done better and been more explicit.
Why is that issue not reopened for fairness?
We have not had many of these proposals in this SIG, and we're obviously not well-practiced in the procedures. The fact that mistakes were made in the past does not mean that repeating those mistakes is the best way forward.
This issue was reopened because people felt that their approval was assumed when they did not intend to have given it yet. I apologize that you're caught in the middle, @muhammad-usama-sardar, and I hope you don't feel like it's directed at you personally. It seems to me as though everyone is just trying to get this driven to an acceptable closure, and I think we'll get there quickly if we focus on any remaining technical points. Thanks again for you patience.
The material difference between this issue and #8 (similarly with #7) is that weeks elapsed for additional feedback once the last feedback was addressed in #8. By contrast, in this issue there was an inaccurate assertion that there was unanimous agreement followed by almost immediately closing the issue. I do not believe there was any ill intent but clearly discussion was not complete.
I do not generally insist on rigid use of voting. If there is general consensus and enough time to let that become evident that is often fine. The word unanimous implied a vote and if there is a vote then it must be recorded.
In open source it's good to keep a few things in mind... Most communication is asynchronous. Someone might not read your last reply for days or even weeks. Whatever is obvious to you may not be for others in the community.
Consequently it is necessary to act with patience and respect.
Approval can be reasonably inferred from the comments of 3/5 chairs, but we should have done better and been more explicit.
So we have explicit approval of 3/5 chairs (@thomas-fossati, @KeithMoyer, @gkostal) for his project also. The clarifications asked by the 4th chair (@shnwc) have been clarified and I have not seen the 5th chiar (@MikeCamel) in the meetings since one year. So why can't approval can be reasonably inferred here?
I hope you don't feel like it's directed at you personally.
The way it was executed clearly shows a personal hit!
remaining technical points
I don't see any remaining technical points. Could you please help me see them?
Consequently it is necessary to act with patience
Did you mean the same patience that you showed for your project In the interim co-chairs please get your feedback/approval into https://github.com/CCC-Attestation/governance/issues/8 I would love to list this RA-TLS harmonization as an accomplishment for the year.
(Quoting you from Slack on #attestation on 09.12 at 11:03 AM)
and respect.
Did you mean the same respect that you showed here? The phrasing, especially whether or to proceed
, is the most disrespectful thing I could imagine. Well, there may be small differences in understanding or formal approval but there was definitely no concern shown on the final scope. It would be hard to imagine something scoped by the chairs themselves as not approved.
There were much better ways of doing this. You could have reached out to me to clarify that hey, I think attestation is not a protocol, could we set up a short meeting to clarify the things, and I would have loved to discuss. Or you could have taken me in loop with the chairs for clarification over email, or you could have asked for a public vote in the SIG meeting. There were various respectful ways of doing it, and you unfortunately chose the most disrespectful one!
As agreed in off-line discussions I am now closing this issue since it's become too hard to follow.
@muhammad-usama-sardar you are welcome to create another issue with your proposed charter where the chairs will take a vote. Please, consider the repo "frozen" for the time being.
Thank you all for your patience.
Background material
Previous relevant Attestation SIG presentations:
Relevant IETF/IRTF discussions:
Proposal
Formal specification and analysis of all phases of attestation mechanisms in Confidential Computing using ProVerif for the following TEEs:
The deliverables for each of the above TEEs are as follows:
Proponents
Muhammad Usama Sardar (@muhammad-usama-sardar)