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 <kerdez...@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, extremely difficult. > Perhaps on a sub-project like libpq ? > > > -- > Laurent "ker2x" Laborde > > On Wed, Dec 8, 2021 at 3:45 PM Colin Gilbert <colingilber...@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 >> >> > >
