Open sdsen opened 1 year ago
@Theophilusbenson @sebymiano @LCastanheira-1 For creating the test harness (Steps 4-10) for extracted modules, wanted to get your thoughts if it would make sense to re-use the klee based machinery Sebastiano and Lucas have been working on.
The Klee-based tool would be helpful in "generating the important" input packets that would provide high confidence. Right now, workflow doest not specify how the input packets should be generated.
@sebymiano I believe you have some insights on how to run an eBPF program in isolation without running the whole kernel! can you provide some pointers?
@Theophilusbenson yes, that's correct. Basically, if we have a script that generates the input packets to be passed to the extracted function, we can reuse the same code that I have written for the equivalence checking to test the function and compare the outputs of the original and extracted function.
The code is here.
What we need to do specifically for this is to modify in this code the way it reads the input packet (here), since right now it reads the KLEE generated file to get the input packet.
@sebymiano the code snippets are in private repo, can we share the same for others to check ?
@sebymiano the code snippets are in private repo, can we share the same for others to check ?
@sdsen the repo is public now, the others should be able to check it out.
@sdsen I have a question regarding the approach you proposed. What you want to do is to show equivalance between extracted function/module and the original one when running as part of a larger monolith.
From the technical point of view, this can be done using the bpf_prog_test_run
for both modules, injecting a specifically crafted input packet to both functions and compare their outputs. This can be done in the same way I did it in the link sent in the previous reply.
The question I have is, when running the original
function which is part of a larger monolith, you should run the entire monolith
, which in turn calls your target function. The entire program can perform other tasks, and potentially modify the input packet. How do you check the equivalence of that specific function, without extracting it before?
@dushyantbehl please track test harness work in this issue.
Is your feature request related to a problem? Please describe.