GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
15 stars 2 forks source link

Assess feasibility of Target1 as an example of a component in a communicating system #400

Closed thebendavis closed 1 month ago

thebendavis commented 2 months ago

Context: historically, pate has been used to understand the implications of a patch applied to a target program. We'd like to also be able to use pate to understand the implications of a patch applied elsewhere in a system of communicating components such that it impacts the performance of a target binary. For example, if a communicating component has been patched such that the length field will always be bounded and valid, could pate be used to characterize the impact on a program's possible behaviors?

The first step is to identify a realistic target program and appropriate goals for pate. This issue is to track studying the Target1 example - see the README for this target for details about the existing issue with length fields in RR_ReadTlm_Input. Does pate self-equivalence work on this target and function? What plausibly might we want to model here? What overrides or other models might we need to add? etc.

thebendavis commented 2 months ago

In an offline discussion, we determined that Target1 is plausibly an example of a program we could use to explore these ideas.

The next thing to do is to explore running pate on Target1 to see if there are any code discovery issues (e.g. unsupported instruction types) that would be a barrier to analysis of the relevant behavior in Target1.

lcasburn commented 2 months ago

From @danmatichuk

Next:

Done when the analysis calls the appropriate function that retrieves the packet w/ no code discovery issues.