Re: Appetite for Frama-C annotations?

This is a longer-term plan and I'm going to practice a lot on my own
projects prior. I'm just sending out feelers. My main idea was to
annotate parts of the code that have already been well-established and
validate it while trying to uncover potential edge-cases. I'll do that
at home until something real comes up. If I find a CVE, I know the
address to send that to. An existing project involves other people and
I cannot expect a free hand to dramatically modify the code everyone
else works upon, especially without having proven my worth! I'm
actually really glad for Laurent's suggestion of checking out libpq; I
assume it sees the least rework? That might actually be a fine first
target for some bug-hunting.

As an aside, my desire to validate the FTS is due to its relatively
exposed nature. This is worrying compared to attacks requiring the
ability to craft special tables, prepared statements, or other things
only a developer or admin could do. Would a memory-safe text search
using the existing data structure be best implemented as a plugin?
I've seen adverts for FPGA IP that can access the Postgres data
structures directly from memory so that gives me confidence. Chapman
mentioned polyglot programming; would Postgres ever consider
deprecating unsafe features and replacing them with plugins written in
something like Rust or Ada/SPARK? I write this, hoping not to tread on
a landmine.

I appreciate everyone's engagement!


Colin

On Thu, 9 Dec 2021 at 14:00, Laurent Laborde <kerdezixe@gmail.com> wrote:
>
> Hi there,
>
> I played a lot with frama-c a long time ago.
> Frama-c annotations are very verbose and the result is highly dependent on the skills of the annotator.
>
> Keeping it up-to-date on such a large project with high-speed development will be, in my very humble opinion,
extremelydifficult.
 
> Perhaps on a sub-project like libpq ?
>
>
> --
> Laurent "ker2x" Laborde
>
> On Wed, Dec 8, 2021 at 3:45 PM Colin Gilbert <colingilbert86@gmail.com> wrote:
>>
>> I've been becoming more and more interested in learning formal methods
>> and wanted to find a good project to which I could contribute. Would
>> the development team appreciate someone adding ACSL annotations to the
>> codebase? Are such pull requests likely to be upstreamed? I ask this
>> because it uses comment syntax to express the specifications and some
>> people dislike that. However, as we all know, there are solid
>> advantages to using formal methods, such as automatic test generation
>> and proven absence of runtime errors.
>>
>> Looking forward to hearing from you!
>> Colin
>>
>>
>
>