Project Veraison (VERificAtIon of atteStatiON)
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Subtitle |
| |
| Title of Series | ||
| Number of Parts | 542 | |
| Author | ||
| License | CC Attribution 2.0 Belgium: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/61470 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | |
| Genre |
FOSDEM 2023308 / 542
2
5
10
14
15
16
22
24
27
29
31
36
43
48
56
63
74
78
83
87
89
95
96
99
104
106
107
117
119
121
122
125
126
128
130
132
134
135
136
141
143
146
148
152
155
157
159
161
165
166
168
170
173
176
180
181
185
191
194
196
197
198
199
206
207
209
210
211
212
216
219
220
227
228
229
231
232
233
236
250
252
256
258
260
263
264
267
271
273
275
276
278
282
286
292
293
298
299
300
302
312
316
321
322
324
339
341
342
343
344
351
352
354
355
356
357
359
369
370
372
373
376
378
379
380
382
383
387
390
394
395
401
405
406
410
411
413
415
416
421
426
430
437
438
440
441
443
444
445
446
448
449
450
451
458
464
468
472
475
476
479
481
493
494
498
499
502
509
513
516
517
520
522
524
525
531
534
535
537
538
541
00:00
Student's t-testProjective planeNetwork topologyPresentation of a groupNeuroinformatikDecision theoryComputer animation
00:46
Term (mathematics)GradientAxiom of choiceVisualization (computer graphics)Natural numberArmMultiplicationGroup actionNeuroinformatikWorkstation <Musikinstrument>Open sourcePointer (computer programming)Projective planeOpen setArithmetic meanCondition numberLevel (video gaming)MereologyRepresentation (politics)Metric systemComputer configurationFormal verificationWordPresentation of a groupQuicksortLink (knot theory)Moment (mathematics)InformationTerm (mathematics)Graph coloringCore dumpComputer architectureCodeOvalCapability Maturity ModelPhase transitionElectronic mailing listMathematicsOnline chatEmailBounded variationGreen's functionWeb pageComputer animation
03:29
Pointer (computer programming)Performance appraisalArithmetic progressionQuicksortWechselseitige InformationArmWorkstation <Musikinstrument>RankingRemote procedure callFormal verificationRow (database)AuthenticationFirmwareGroup actionNeuroinformatikIdentity managementComputer hardwareSoftwareKey (cryptography)RootComputer architectureDecision theorySoftware testingResultantRight angleState of matterFunction (mathematics)Frame problemLink (knot theory)ChainCuboidInternet service providerProcess (computing)Patch (Unix)Computer configurationCASE <Informatik>Connectivity (graph theory)Cartesian coordinate systemComputing platformWorkloadComponent-based software engineeringPhysical systemConfiguration spacePublic-key cryptographyComplex (psychology)MultiplicationDifferent (Kate Ryan album)Functional (mathematics)Line (geometry)Axiom of choiceSign (mathematics)MeasurementMathematicsSpectrum (functional analysis)Information privacyInstance (computer science)Real numberLogicSensitivity analysisDuality (mathematics)Order (biology)Communications protocolPerformance appraisalTraffic reportingElectronic signatureArithmetic meanInterpreter (computing)2 (number)1 (number)Information securityFormal languageMassInformationMereologyNatural numberTwitterExtension (kinesiology)Degree (graph theory)Revision controlFlow separationFood energyGoodness of fitVisualization (computer graphics)Condition numberRule of inferenceMachine visionReflection (mathematics)Boss CorporationLocal ringPhysicalismSeries (mathematics)Web syndicationComputer animationDiagramProgram flowchart
10:34
Performance appraisalCanonical correlationCommercial Orbital Transportation ServicesComa BerenicesOpen setPoint (geometry)View (database)Codierung <Programmierung>Sign (mathematics)Software testingForm (programming)Group actionFunction (mathematics)InformationDemo (music)Endliche ModelltheorieDataflowINTEGRALForcing (mathematics)Standard deviationMultiplication signCivil engineeringGoodness of fitLatent heatLine (geometry)CuboidSoftwareInterface (computing)FirmwareLibrary (computing)ResultantDifferent (Kate Ryan album)Dimensional analysisComputing platformNeuroinformatikFile formatProxy serverImplementationArmFront and back endsElectronic mailing listProfil (magazine)Product (business)Projective planeComputer architectureIntegrated development environmentCartesian closed categoryPerformance appraisalOcean currentEmulatorNormal (geometry)Decision theoryGibbs-samplingCellular automatonAdditionFamilyWorkstation <Musikinstrument>Service (economics)TrailBlock (periodic table)Boss CorporationPrisoner's dilemmaCASE <Informatik>Computer animationProgram flowchart
14:41
Vapor barrierService (economics)Projective planeConnectivity (graph theory)Library (computing)Formal verificationPhysical systemFormal languageDemonRight angleMappingGoodness of fitPattern languageTerm (mathematics)CurveRevision controlAxiom of choicePoint (geometry)FreewareDiscrete element methodDigitizingComputer animation
15:58
UsabilitySign (mathematics)Limit (category theory)Process (computing)Decision theoryPoint (geometry)GoogolMoment (mathematics)ArmRevision controlMusical ensembleSoftware frameworkNumberMessage passingDemosceneInterface (computing)Keyboard shortcutCuboidPerformance appraisalInformationService (economics)Formal verificationLevel (video gaming)Form (programming)Lie groupFormal languageFreezingKey (cryptography)SoftwareConfidence intervalFreewareTime zoneCondition numberProjective planeBlogDigital photographyTwitterWebsiteVideo gameForcing (mathematics)Graphical user interfaceProfil (magazine)Arc (geometry)ResultantStandard deviationRight angleClient (computing)Line (geometry)EmulatorBlock (periodic table)QuicksortShape (magazine)File formatLatent heatInformation securityBuildingImplementationMultiplication signOpen setTemplate (C++)Dependent and independent variablesCommitment schemeTerm (mathematics)Beat (acoustics)XML
20:58
Performance appraisalFile formatComputer architectureQuicksortCore dumpService (economics)Group actionGreatest elementHookingBitSurfaceVector potentialIdentity managementGeneric programmingPoint (geometry)UsabilityOrder (biology)CodeMultiplicationProcess (computing)Formal verificationFile formatMultiplication signProduct (business)Context awarenessPlug-in (computing)VideoconferencingStandard deviationINTEGRALInformation securityBeat (acoustics)Bounded variationRight angleArmLevel (video gaming)NeuroinformatikDialectCondition numberForm (programming)Event horizonData managementData storage deviceBuildingFluid staticsElectronic mailing listComputer animationProgram flowchart
23:37
Computer animationProgram flowchart
Transcript: English(auto-generated)
00:05
Okay. Hi. My name is Thomas, I'm engineer term. I'm also a contributor to the project very reason. This presentation is about very reason, and once you get to give you a, an idea of what the project is about, and how it fits in the weather destination slash confidential computing picture.
00:26
With the hope that, you know, after after listening to this you'd be motivated to at least have a look at the project and maybe become an early adopter, or even a contributor in the future. Who knows. So, without further ado, let me go through what I've put together here, starting with a bunch of trees via about the project.
00:47
So we have a logo. And the colorful ovals there are supposed to represent grapes. In fact, for reason is a term used in winemaking. And is the moment when grapes start frightening.
01:02
At which point, they can be of different colors. And in fact the word means change of color. And this is sort of visual metaphor of the blurry nature of trust, which can be yes can be no green grape grape, or really anything in between. Now there's some debate around the way the word is pronounced the French say very soon.
01:25
The reason the English save the reason or variation. So you have a choice. I have multiple choices. In fact, please do not spell it like the American company because that would be really confusing. And it's also a background in for verification of attestation project started within
01:45
arm in the architecture and technology group that we should belong to my colleagues are on the team as well. It's been adopted by the confidential computing consortium in June, 2022 is currently in incubation stage, meaning
02:04
is in the early phases of adoption and we're looking at growing it across a few different metrics. The most obvious being code and documentation maturity. But also, we are also trying to grow the community a bit.
02:23
And being here is part of that effort. But yeah, the headline here is that we've moved from being in our project to be under the Linux foundation umbrella. Therefore, we're completely open governance and of course open source.
02:41
Before we dive into the core of the presentation, though, let me give you a bunch of pointers, possibly useful. The code base gets up the chat, the chat mailing list hosted by the confidential computing consortium. And these confusing URL, which is one for our regular weekly calls, which I'm not expecting
03:03
you to memorize In fact, you could you could just follow the could just follow the. The first link in the list, the GitHub org and the splash page should have all of these other links. But, you know, general feel free to join any of these channels pop up at our calls, ask questions, whatever you will be always very much welcome.
03:30
So now we do a quick recap on remote devastation. Starting with the problem. And so you suppose you have these two guys attached to an underlying party that needs to engage in some sort of distributed computation.
03:42
Suppose also that initially they are. They don't trust each other mutually distressing. And then you can't make progress in the competition until a trust relationship is can be established within the two. And instances of this kind of situation abound, for example, in confidential computing. The tester is typically the guy that executes the workload, the confidential workload, and the live
04:05
party needs to know that these guys is trusted before it shares some input with it. Say for example, you know, you need to ship an ML model, or some privacy sensitive data, or both. And there's obviously obviously the, the, the, the, the dual problem right we are
04:25
where we are the party is the consumer of the output of the competition. So you are an actuator of some sort of that acts upon signals that are coming from the tester, and you want to trust the tester before making a mess right so you stuff in critical infrastructure, especially.
04:42
So to break this impasse, the natural thing to do is for one party to convince the other that they can be trust. And here's where attestation comes in the frame so decision, what is that decision is a technique that uses specialized specialized component,
05:02
which is rooted in hardware called the root of trust that the tester can use to do basically two things, the sampling the current state of its PCB is trusted computing base and and put together a report and and be signed this record with with the secret identity keys that are securely stashed inside the root of trust in hardware.
05:27
All of that in a trustworthy way. Now that isn't in such a way that no one even co located software or firmware can subvert these secrets of actions. And this signed record is called attestation evidence or people evidence.
05:42
And the evidence which is, you know, basically a very very strong authentication signal can be sent to the RP which, you know, once it receives it needs to verify by by checking that the very the signature of the report is correct, and that the identity
06:02
of the signer is known and trusted, and also to check that the reported PCB state is acceptable, slash good for some local policy defined interpretation of what good means. And the process of verification of evidence is the process that covers at least these two checks that we just
06:24
discussed. And in the remote attestation architecture, which is RFC 9334, freshly published. This process of verification of evidence is taken care of by the verifier role, which basically mediates between testers and relying parties.
06:43
Know that the, the, the lines in in in this picture are not real channels between real devices they are logical channels between architecture roles, so they can be recomposed and put together in a very different way depending on the protocol.
07:01
Logically, these are the relationship is between between various architecture roles. Um, um, and in order to do to his function the verifier needs to know a few things few very important things. First, how to verify the identity of a tester.
07:21
Typically that is done by knowing a public key associated with the secret signing key of the tester and knowing that in a reliable way. And and be what is the expect expected state of get tested PCB. Of course,
07:42
and this can become pretty messy depending on how complex the tester is on one end of the spectrum you have very simple testers that can be described with a single measurement does not change or changes glacially. And on the other hand, there are, you know, composite testers that are made of more than one a tester,
08:03
each a tester sporting its own TCP HTTP made of multiple separate independently moving parts, you know, software components configuration whatnot. With multiple different supply chain actors involved, you know, thinking become really hairy.
08:20
So, if the complexity is very low, it makes sense to call Kate a simple verifier with the line party but if that's not the case, you know, it might be a reasonable choice to design a system where the verification function is effectively offloaded to a separate architectural component.
08:41
These options are not, you know, aggregation desegregation, or did they are not mutually exclusive. Take for example the case where the tester is composite and it's evidence can be clearly split along a platform slash workload axis. So, in that case, one might want to call an external platform verifier, and if
09:04
everything is okay then move to a local verifier for for the verification of the workload. You know, there. As I said, the things are logical they can be reassembled and put together in very very different way. But in general, whatever the system architecture and you come up with the verifier role needs a bunch of trusted
09:23
links to the supply chain that is involved in, in, in, in, in the verification, because the splashing endorses the tester. Right. And so it's critical that the link between the supply chain and the verifier is is a trusted one.
09:45
And that endorsements are genuine. And these are the green boxes in this picture. But if I could also have an owner, typically have an owner that can provide verification policies for evidence to
10:01
it, save for you know to customize the process of appraisal or, you know, in special situations, maybe provide a patching. And to complete the rats architectural picture is the IP owner, relying party owner can feed the policy for how to act on the attestation results coming from the verifier right to
10:25
extract the right party to make decisions based on on the appraisal done by the verifier regarding the tester. So this finishes the rats recap. And the question now is, is where is very in this picture.
10:43
And as you may have guessed, is the blue box at the center. But it's not just that it's also all the lines that are attached to the blue box that is all the verifier interfaces which are quite a few. So from the bottom left, and then move.
11:00
But why. So evidence we've built a bunch of libraries for manipulating various evidence formats, both from point of view of the verifier so the coding and verification, but also from the tester point of view, which means encoding and signing this way. If one needs to put together an end to end flow safer integration testing or for the demo it's quite easy to build this, you know, tester emulator.
11:25
You don't need to deal with the real horror, which can be tricky, especially if you're dealing with CI environments. The current list of supported evidence includes to eat profiles PSA for cortex them. So it gives more and NCCA for the new arm v9 confidential computing architecture.
11:44
We also have a TPM profile, and this came from an integration project we did with our friends at inactive trust, who have a product for monitoring device health that can use reason as a back end. We have a bare bones implementation of dice.
12:02
See TCG but open is okay. I think. And then we have AWS nitro. Contributed by our friends at Veracruz. This is another triple C project that's a confidential computing project that uses for reason as the back end for their proxy CA.
12:26
And, you know, more. Yeah. On endorsement ref value front. We have implementation for Corinne, which is a format we could design with Intel and from hopeful in the dice working group in TCG,
12:43
and has now been adopted in the ATF rats working group, as you know, on the on the standards track is basically a specialized former for for describing the, how the how the tester looks like to to to verify, which aggregates different sub formats for specifying bunch of, you know, we're talking about cool.
13:11
Oh existing dimensions of the platform so software firmware trust anchors, other things. For policy we have integrated the open, open policy agent, which is an existing successful general purpose policy engine.
13:27
So, we found something that existed that was fit for purpose so we didn't, we didn't feel the need for invent this specific bits, and for acquisition results there's an info model that's being standardized in the ATF called a forcey, which allows to normalize
13:47
the appraisal output. So the so that the line party policies can be simplified greatly, because now they're fully coupled from the specifics of the tester.
14:01
But because our forces just an info model we had to create a civilization for it, which we based on it. We call ear. Here is a good candidate for standardization because, you know, just, just nothing. At this point in time. And so we're trying to push this through, through the rest working group you have as well.
14:24
And it's the only output form of support for now. As far as decision. Result policies, we do nothing because this is completely out of scope, this is entirely on the underlying party.
14:41
So yeah, now, I wanted to give you the mapping of what we just discussed with the, with what exists in the reason conveys and know that nearly the entirety of what follows is going packages, and also command line tools and and services slash demons in good old Unix patterns.
15:03
And, and this. This was a conscious choice, we choose to go with going. Because, you know, one of the main goals of the project is to provide a bunch of component three to assemble system that provides verification as a service right so and go I guess is a very good language in terms of library support, native
15:26
library support ecosystem. And, and also the terms of business, you know, you know the learning curve is very is very non steep, I would say, so it's it's it's trivial to learn
15:45
and and for, you know, we hope that more people can be more contributors could be could come by lowering the barrier barrier here. So let's start with a couple of layers zero packages eating go cozy.
16:03
It is the entity decision token is the main format for official messages, either evidence or attestation results that been put forward by the ATF is basically a framework that extends cotton jot by adding a number of claims with attestation specific
16:22
semantics, and also a way to instantiate the framework for so called profiles and PSA and CCA being just, you know, two such examples. The package is very neat package is not tracking the most recent version of the draft.
16:42
We decided to wait for the draft to become out of C before doing a final alignment pass because it has all the claims that we need, you know, for for independent packages and so for for the moment is, is, is good as is. But we will need to, to, to, to make it up to date.
17:03
You know, as soon as the, as soon as the document goes through the standardization process final stages of the standardization process. And it builds on caught, which in terms uses cozy sign and saying one. So early on we realized that we needed a cozy implementation in go. And the only thing we could
17:25
find at the point in time was go cozy, which was originally developed by Mozilla for their autograph service. But it supported only cozy sign. So we forked it and extended to support sign one.
17:40
But then Mozilla discontinued it when the point is that we wanted to, to, to contribute it back to the main line. They discontinued the project so we took responsibility of it alongside Microsoft. And together with Microsoft we did a fair amount of work including improving the ergonomics of the interfaces you know, and also making making implementation generally more robust.
18:06
And to that respect, we went through a couple of external security reviews and address the older comments, so we're fairly confident in that this package as you know, production quality and and we, and we shipped 100, just a couple of weeks ago.
18:25
And this is the first ever released beta varies and so we're particularly excited by that. Um, it's an interesting package among the lot also because it's used not just by Verizon, but also by other quite big projects, not only in CNC f and six store open as a self.
18:48
So we see is a nice, it's come out as a as a nice useful building block that has relevance in the community. Now moving on to the evidence. You know, these are the evidence based the the red, the orange things.
19:06
We have the tweet profiles for CCM PC, PC, the dice thingy, and, and the the sort of house like shape is the common line interface, call a VCLI, which is an attester emulator that also talks of reason verification API client side.
19:25
And so can be used to play with the services quite easily. Come online. The yellow things are the attestation results packages. So here is only one package basically is it's very soon here, and there's an associated CLI arc can be used to verify and pretty print results.
19:47
So one can pipe VCLI outputs into arc to see what's what happened during appraisal. And the green thing is the bunch of endorsement profile related packages, including the top level
20:01
manifest format coding quorum, and the dependent beats for for verification keys and software and so on. So, according commit column quotes and sweet respectively. And also Coakley, which is a common line to face for assembling columns from from a bunch of JSON templates.
20:21
You sign them and then you can submit them to the original services using the provisioning API which is linked into Coakley. And finally, the blue box, including a micro services, which I will talk about in the next slide, and the client side interface of the reason API, which exists, also in rust with C bindings.
20:47
And I think a pure C implementation has been contributed as well. I don't know where, where, if it's been merged fully or is still an open PR right anyway. So, yeah, well let's have a look, quick look at the service architecture.
21:05
Basically, there are two pipelines, one for verification. The bottom one, and one for provisioning that he did the top one that converge on to the core services service. VTS, which connects to the data and the plugin stores.
21:23
It's called videos. It is. This is another winemaking point. And it's basically variations services trusted computing base. It has a whole the security related computation in it.
21:42
The interesting thing is that the, the processing in both pipelines is in stages, and, and with with with very precise hook points were playing code can be supplied by the user in order to customize certain aspects of the processing.
22:01
So basically, what you do is, as a user that wants to add their own format, either of evidence or for endorsements and ref values, you build your plugin code, so that you basically you adapt your formats to the, to the standardized processing pipeline.
22:29
Right. So next steps. The few exciting new things in the pipeline. Adding new formats, of course, opportunistically though, depending on contributions integrations etc.
22:47
We want to improve documentation, not a very exciting bit but a necessary step in making the project useful and usable. And this is a big one, we want to work on the identity and access management to support the, you know, more, the more generic multi tenant service.
23:08
And then this is the single missing beat that prevents reason from being used in a production context at this point in time. And finally want to allow a static plugin less build in order to reduce the potential attack surface on the surface on the on the services.
23:31
Yeah. This is what the next month will bring us. So questions. Thank you very much, by the way, for listening.