Обсуждение: Appetite for Frama-C annotations?
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
Colin Gilbert <colingilbert86@gmail.com> writes: > 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? Most likely not. It might be interesting to see if it's possible to do anything at all with formal methods in the hairy mess of the Postgres code base ... but I don't think we'd clutter the code with such comments unless we thought it'd help the average PG contributor. Which I doubt. > Are such pull requests likely to be upstreamed? We don't do PRs around here --- the project long predates the existence of git, nevermind github-based workflows, so we're set in other habits. See https://wiki.postgresql.org/wiki/Developer_FAQ https://wiki.postgresql.org/wiki/Submitting_a_Patch regards, tom lane
On 12/07/21 13:32, Colin Gilbert 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? My ears perked up ... I have some Frama-C-related notes-to-self from a couple years ago that I've not yet pursued, with an interest in how useful they could be in the hairy mess of the PL/Java extension. Right at the moment, I am more invested in a somewhat massive refactoring of the extension. In one sense, tackling the refactoring without formal tools feels like the wrong order (or working without a net). It's just that there are only so many hours in the day, and the refactoring really can't wait, given the backlog of modern capabilities (like polyglot programming) held back by the current structure. And the code base should be less hairy afterward, and maybe more amenable to spec annotations. According to OpenHub, PL/Java's implementation is currently 74% Java, 19% C. A goal of the current refactoring is to skew that ratio more heavily Java, with as little C glue remaining as can be achieved. Meaning, ultimately, a C-specific framework like Frama-C isn't where most of the fun would be in PL/Java. Still, I'd be interested to see it in action. Regards, -Chap
Hi! Thanks for the quick reply. Are you doing any of this work in a public repository? If so, could we have a link? There is a similar idea in Java Modelling Language. It also uses its own annotations to describe additional requirements. Are you considering to use it? Maybe I could help... On Wed, 8 Dec 2021 at 16:02, Chapman Flack <chap@anastigmatix.net> wrote: > > On 12/07/21 13:32, Colin Gilbert 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? > > My ears perked up ... I have some Frama-C-related notes-to-self from > a couple years ago that I've not yet pursued, with an interest in how > useful they could be in the hairy mess of the PL/Java extension. > > Right at the moment, I am more invested in a somewhat massive > refactoring of the extension. In one sense, tackling the refactoring > without formal tools feels like the wrong order (or working without a net). > It's just that there are only so many hours in the day, and the > refactoring really can't wait, given the backlog of modern capabilities > (like polyglot programming) held back by the current structure. And the > code base should be less hairy afterward, and maybe more amenable to > spec annotations. > > According to OpenHub, PL/Java's implementation is currently 74% Java, > 19% C. A goal of the current refactoring is to skew that ratio more > heavily Java, with as little C glue remaining as can be achieved. > Meaning, ultimately, a C-specific framework like Frama-C isn't where > most of the fun would be in PL/Java. Still, I'd be interested to see it > in action. > > Regards, > -Chap
Thank you very much Tom for your quick reply! If nobody objects to it too much, I'd focus my work on ensuring full-text-search is memory-safe. On Wed, 8 Dec 2021 at 15:21, Tom Lane <tgl@sss.pgh.pa.us> wrote: > > Colin Gilbert <colingilbert86@gmail.com> writes: > > 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? > > Most likely not. It might be interesting to see if it's possible to > do anything at all with formal methods in the hairy mess of the Postgres > code base ... but I don't think we'd clutter the code with such comments > unless we thought it'd help the average PG contributor. Which I doubt. > > > Are such pull requests likely to be upstreamed? > > We don't do PRs around here --- the project long predates the existence > of git, nevermind github-based workflows, so we're set in other habits. > See > > https://wiki.postgresql.org/wiki/Developer_FAQ > https://wiki.postgresql.org/wiki/Submitting_a_Patch > > regards, tom lane
On 12/08/21 12:13, Colin Gilbert wrote: > Hi! Thanks for the quick reply. Are you doing any of this work in a > public repository? If so, could we have a link? There is a similar > idea in Java Modelling Language. It also uses its own annotations to > describe additional requirements. Are you considering to use it? Maybe > I could help... PL/Java's public repository is https://github.com/tada/pljava Much of the current refactoring I spoke of is not pushed there yet (it is still in the getting-rebased-a-lot stages). There may be an initial push of it appearing there in the coming weeks though. JML is also mentioned in my notes from a couple years back when I was browsing such tools. There is also a PL/Java-specific mailing list at https://www.postgresql.org/list/pljava-dev/ The traffic there is not high. Regards, -Chap
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 <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
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 >> >> > >
On 12/09/21 12:53, Colin Gilbert wrote: > ... plugins written in > something like Rust or Ada/SPARK? I write this, hoping not to tread on Some work toward supporting "deep" PostgreSQL extensions in Rust was presented at PGCon 2019 [0]. Regards, -Chap [0] https://www.pgcon.org/2019/schedule/events/1322.en.html
Chapman Flack <chap@anastigmatix.net> writes: > On 12/09/21 12:53, Colin Gilbert wrote: >> ... plugins written in >> something like Rust or Ada/SPARK? I write this, hoping not to tread on > > Some work toward supporting "deep" PostgreSQL extensions in Rust > was presented at PGCon 2019 [0]. There's also https://github.com/zombodb/pgx/, which seems more complete from a quick glance. https://depth-first.com/articles/2021/08/25/postgres-extensions-in-rust/ - ilmari
Thank you all very much for your inputs! To summarise: I asked about the possibility of adding ACSL annotations to the codebase and the responses ranged from nonplussed on one end of the spectrum to some degree of enthusiasm on the other. It was suggested that libpsql would be a better initial target than the internals. I appreciated the good, brisk discussion and if anyone else has any other ideas please let us all know. Regards, Colin