Hardening SunRPC XDR encoding and decoding

[chucklever]

Given recent advances with RPC-with-TLS, I would like to verify the XDR encoder and decoder functions in the Linux NFS server as part of introducing support for transport-layer security. The Linux NFS server implementation is open-coded in C and does not rely directly on the XDR language snippets provided in the NFS specifications. Formal proof is one approach, but I'm a rank beginner in this area. Any advice appreciated!

[nikswamy]

Hi there, sorry for the slow response.

If you're interested in obtaining verified C code for just the decoders, one approach might be to use EverParse/3D.

See this paper: https://www.fstar-lang.org/papers/EverParse3D.pdf

If you could provide some specifics about the fragments of XDR that you're particularly interested in, perhaps with some samples, I'd be happy to comment a bit more on the feasibility using EverParse.

[chucklever]

That paper is what got me interested in your efforts.

One of the less complex areas that has been of particular concern is parsing and forming NFSv3 READDIR requests and replies. You can see the XDR definition of NFSv3 READDIR in Section 3.3.16 (and 3.3.17) of RFC 1813.

[nikswamy]

That's really interesting ... thanks for the pointer and for making the connection.

I think it should be relatively easy to write a specification in 3D for formats of this flavor. But, the delicate balance to strike is to write the specification in a style that makes it possible to slot the generated C code in to some existing code base, matching as much as possible the current APIs etc.

Do you think you could also point me to a bit of existing Linux code that tries to parse such requests. Also, you mention that this has been an area of particular concern: have there been bugs reported in this space? If so, could you point me at the bug reports ... it would help me gauge whether doing this with 3D would allow one to rule out bugs of a similar class in the future.

[chucklever]

Slotting generated code into the Linux kernel's XDR infrastructure is a major concern. You can see the current server-side NFSv3 decoders and encoders here: nfs3xdr.c. The READDIR encoder in particular is nfs3svc_encode_readdirres(), and the per-directory entry encoding is done by nfs3svc_encode_entry3().

A set of pages is allocated for each Reply and set up as the buffer that receives each encoded element. The state of the encoding is managed in a struct xdr_stream (svc_rqst::rq_res_stream).

A few recent bugs in this code:

• 640f87c190e0
• 53b1119a6e50

[nikswamy]

You might also find this useful: https://project-everest.github.io/everparse