This PR provides support for a "probe and copy" feature, allowing input formats to contain pointers that will be followed by the validator after a user-provided "probe" function checks that the pointer refers to legal memory for a given extent.
The following example illustrates (from tests/Probe.3d)
extern probe ProbeAndCopy
typedef struct _T {
UINT32 x { x >= 17 };
UINT32 y { y >= x };
} T;
entrypoint
typedef struct _S(EVERPARSE_COPY_BUFFER_T dest) {
UINT8 tag;
T *t probe (length = 8, destination = dest);
} S;
You can declare an extern probe function, say ProbeAndCopy. In the generated C code, we produce the following extern declaration for it, which you can provide at link time:
This function should probe the pointer_value, and if successful, it will copy length bytes into destination. You can use whatever existing (typically kernel) primitive you have for this and it should take care of the exception handling etc. and just return a boolean.
In the specification of the type S above, we take a EVERPARSE_COPY_BUFFER_T dest as an argument.
The field t of S is a pointer to a T, and the annotation says that it should be probed and copied (using the declared ProbeAndCopy in scope) and then the contents of dest will be validated to contain a T.
At the top-level, EverParse gives you the following function to validate an S. When calling it from C, you should make sure that dest does not alias base (or any other out parameters you may have).
This required a change to the abstraction of validators and actions. Now, they are indexed by an additional "disjointness precondition", which is used ensure that when validating the contents of a copy buffer, that an action running during that process does not modify the copy buffer itself. For example, the disjointness precondition causes us to (rightfully) reject this specification---to validate S *s we copy into dest, but in the process of validating S we again copy into dest when encountering T *t. This is detected and rejected.
//Nested probing of the same buffer; should fail
entrypoint
typedef struct _R(EVERPARSE_COPY_BUFFER_T dest) {
UINT8 tag;
S(dest) *s probe (length = 9, destination = dest);
} R;
Compiler performance
The addition of the disjointness precondition adds an overhead to the verification of all 3D specs, even those that do not use copy buffers, since the abstraction forces us to compute the disjointness precondition anyway. On small specifications, this overhead does not seem to be observable significantly. However, on a large internal benchmark, I measured an end-to-end overhead of around a 20% slowdown in verification time. I am still contemplating ways to reduce that overhead, though at least some overhead seems unavoidable, since we do have to compute this disjointness precondition for soundness. Perhaps there's a way to avoid computing it for the common case in which probing is not used.
This PR provides support for a "probe and copy" feature, allowing input formats to contain pointers that will be followed by the validator after a user-provided "probe" function checks that the pointer refers to legal memory for a given extent.
The following example illustrates (from tests/Probe.3d)
This function should probe the pointer_value, and if successful, it will copy length bytes into destination. You can use whatever existing (typically kernel) primitive you have for this and it should take care of the exception handling etc. and just return a boolean.
In the specification of the type
S above, we take aEVERPARSE_COPY_BUFFER_T destas an argument.The field
t ofS is a pointer to aT, and the annotation says that it should be probed and copied (using the declaredProbeAndCopy in scope) and then the contents ofdest will be validated to contain aT.You chose how to implement EVERPARSE_COPY_BUFFER_T: EverParse.h defines
typedef void* EVERPARSE_COPY_BUFFER_T. So, you can implement that type as you like and call the validator with a pointer to your type; a typical choice is that it can itself be a UINT8* with a length. See https://github.com/project-everest/everparse/blob/8572ec9cf8d3abb49ac76e2a218dbf7fcbb48fbc/src/3d/tests/probe/README.md for more details.At the top-level, EverParse gives you the following function to validate an
S. When calling it fromC, you should make sure thatdest does not aliasbase (or any other out parameters you may have). Disjointness preconditions
This required a change to the abstraction of validators and actions. Now, they are indexed by an additional "disjointness precondition", which is used ensure that when validating the contents of a copy buffer, that an action running during that process does not modify the copy buffer itself. For example, the disjointness precondition causes us to (rightfully) reject this specification---to validate
S *swe copy intodest, but in the process of validatingSwe again copy intodestwhen encounteringT *t. This is detected and rejected.Compiler performance
The addition of the disjointness precondition adds an overhead to the verification of all 3D specs, even those that do not use copy buffers, since the abstraction forces us to compute the disjointness precondition anyway. On small specifications, this overhead does not seem to be observable significantly. However, on a large internal benchmark, I measured an end-to-end overhead of around a 20% slowdown in verification time. I am still contemplating ways to reduce that overhead, though at least some overhead seems unavoidable, since we do have to compute this disjointness precondition for soundness. Perhaps there's a way to avoid computing it for the common case in which probing is not used.