[saag] Re: [nasr] Re: Re: Re: Re: NASR BOF Follo w-Up

Hi Watson,

The term "nontrivial semantic claims" can refer to many complex and even unproveable claims, and we fully acknowledge that we cannot provide all such advanced claims. Only a new domain-specific language could serve as an intermediate layer to formally bridge the significant gap between the simple claims provided by RATS and all "nontrivial semantic claims"—but that would clearly be boiling the ocean and beyond our current capabilities.

NASR does not aim to deliver all possible "nontrivial semantic claims" or provide a fully complete theoretical framework. Instead, we focus solely on those claims that can be derived through simple composition and basic reasoning from the original RATS claims—what we call "one more step" inferences. Here are some examples that we want to present to the counterparties (customers, supervisors... ):

--  All L3 devices along this flow have used secure boot capability
--  All L3 devices along this flow are deployed in country Germany or AS3320
--  All interfaces traversed by this flow are encrypted with MACSEC, using a Post-Quantum Suite

And so on. And also Eric's these examples in another thread that I quote: 

	* This traffic was sent over an encrypted link
	* All traffic to address X will be sent over an encrypted link
		Yes. 
	* This traffic is not being sent to a spanning port or otherwise available for monitoring
		Slightly harder, under an assumption that you believe remote attested devices will always behave deterministically as the configuration indicates, and will not do anything else (unexpectedly).

Peter

> -----Original Message-----
> From: Watson Ladd <[email protected]>
> Sent: Wednesday, May 21, 2025 3:39 AM
> To: Meiling Chen <[email protected]>
> Cc: Henk Birkholz <[email protected]>; Liuchunchi(Peter)
> <[email protected]>; ekr <[email protected]>; Toerless Eckert
> <[email protected]>; [email protected]; IETF SAAG <[email protected]>; Luigi Iannone
> <[email protected]>
> Subject: Re: [nasr] Re: [saag] Re: Re: Re: NASR BOF Follow-Up
> 
> On Tue, May 20, 2025 at 4:32 AM Meiling Chen
> <[email protected]> wrote:
> >
> > Hi Watson,
> > I'm confused about "nontrivial semantic claims", can you give an example
> to explain?
> >
> > For example, if the operator's customer requires every node to support
> TEE, then only need to choose from nodes that have TEE functionality. It is
> not necessary to determine whether the router supports TEE from each
> configuration and operation directive, and to ensure the authenticity of the
> claims supporting TEE functionality, that's in the scope of RATS.
> 
> Correct. Some claims are easy to verify. Most aren't. Statements that "the
> router supports X" aren't really interesting. Statements that "this
> configuration will never pass your traffic over a bad link" are, but are a lot
> harder to show.
> 
> >
> > Best,
> > Meiling
> >
> > From: Watson Ladd
> > Date: 2025-04-19 02:22
> > To: Henk Birkholz
> > CC: Liuchunchi(Peter); Eric Rescorla; Toerless Eckert; [email protected];
> > IETF SAAG; Luigi Iannone
> > Subject: [nasr] Re: [saag] Re: Re: Re: NASR BOF Follow-Up Dear Henk,
> >
> > Your response was very detailed I think helped me at least, understand
> > the core issue of our disagreement. If I might take some liberties in
> > summarizing, it sounds like what you want is to provide additional
> > scaffolding from NASR to enable collection of evidence, and maybe some
> > standardized ways to represent the evidence, from a chain of routers
> > that it can be proved some packets transit. The evidence attests to
> > syntactic properties of the code and configuration at a point in time,
> > maybe with some kind of history mechanism to understand it.
> >
> > However, the properties being claimed are nontrivial semantic claims
> > dependent on the configuration and the software that uses this
> > configuration to route packets. There's a big gap here, and I don't
> > believe it has been solved. To the extent that NASR needs these to be
> > solved to provide certain things, it won't be able to provide them,
> > and I think that undermines a lot of the presented rationale.
> >
> > Sincerely,
> > Watson Ladd
> >
> 
> 
> 
> --
> Astra mortemque praestare gradatim
_______________________________________________
saag mailing list -- [email protected]
To unsubscribe send an email to [email protected]