4 ms·

> I found 4 different Postgres bugs. Bugs in the upstream Postgres C implementations? Did you report them or submit patches? I'm curious to see what you found!

malisper 2mo ago
Yep, I did submit bug reports. This was on Tuesday. I don't see a public copy of the mailing list that has my bug reports yet. The four bugs were: 0) When parsing a macaddr[0], Postgres uses sscanf with %x. %x can wraparound. This means SELECT '10000000aa:bb:cc:dd:ee:ff'::macaddr; will return aa:bb:cc:dd:ee:ff. 1) When parsing a tid[1], Postgres uses strtoul. The return value of strtoul is different across platform for the empty string. This means on some platforms Postgres SELECT '(,5)'::tid; will error and others will accept it. 2) Postgres missed an overflow check in it's cash type[2]. When running SELECT '-92233720368547758.08'::money / (-1)::int8; some platforms will error and other's will return the MIN value. Postgres does check for this for some of the other cash related functions, but it missed it for one of them. 3) When hashing the "char" type Postgres will cast a char to an integer[3]. On some platforms char is signed and on others it's unsigned. This means the hash of a char can be different depending on the platform. If you are using a hash index or hash partitioning on a char and move your DB from x86 to arm, the hashes will differ and your index/partitioned tables become corrupted. Note that this is special char type that you have to refer to by "char" that is separate from the typically used CHAR(n) type which is what you typically use, hence this would never come up under real usage. The common pattern with all of these is they rely on C behavior that differs across platform (integer overflow, char signedness, strtoul). Rust is better about having more consistent behavior across platforms so these cases get flagged when the Rust code and the C code differ. [0] https://github.com/postgres/postgres/blob/REL_18_3/src/backend/utils/adt/mac.c#L71-L81 https://github.com/postgres/postgres/blob/REL_18_3/src/backe... [1] https://github.com/postgres/postgres/blob/REL_18_3/src/backend/utils/adt/tid.c#L75-L81 https://github.com/postgres/postgres/blob/REL_18_3/src/backe... [2] https://github.com/postgres/postgres/blob/REL_18_3/src/backend/utils/adt/cash.c#L155-L165 https://github.com/postgres/postgres/blob/REL_18_3/src/backe... [3] https://github.com/postgres/postgres/blob/REL_18_3/src/backend/access/hash/hashfunc.c#L47-L51 https://github.com/postgres/postgres/blob/REL_18_3/src/backe...
- appplication 2mo ago
  Very cool project and good finds. What do you see as the end state for your project - do you think pg has a path to upstream, or would this be a fork? Without knowing anything about the pg team, I would assume they would be hesitant to even consider an under the hood switch, just from a risk management perspective, regardless of test coverage and formal verification. But I could be wrong.
  - malisper 2mo ago
    Thank you for the kind words! My goal is to build the best database possible. I'm trying to imagine what Postgres would be like if it were built today. I've been able to make a bunch of big architectural changes that the Postgres team has been talking about but hasn't yet made. For example, threads instead of processes and a vectorized executor. I think everyone would agree the types of changes I'm making are good ones. The challenge Postgres faces is there's millions and millions of Postgres databases out there so they are focused on minimizing the risk of breaking any existing functionality over doing a big high risk rearchitecture. I could see ideas from what I'm doing gradually making their way into Postgres, but I think the odds that pgrust (or any Rust code for that matter) gets merged into Postgres is close to zero.
    - wonger_ 2mo ago
      For other interested spectators, I found this post by the author to be a good example of architectural changes in pgrust (along with motivations): https://malisper.me/the-four-horsemen-behind-thousands-of-postgres-outages/ https://malisper.me/the-four-horsemen-behind-thousands-of-po...
- throwaw12 2mo ago
  these are impressive findings, I am curious what was your process to convert existing code to formal verification languages like TLA+. My basic understanding was to verify high level abstractions (e.g. transport ACK, fsyncs and so on), but verifying this deep probably requires complete verification of stdlib methods used by Postgres, otherwise how can you pinpoint culprit is the sscanf?

malisper 2mo ago

Yep, I did submit bug reports. This was on Tuesday. I don't see a public copy of the mailing list that has my bug reports yet. The four bugs were: 0) When parsing a macaddr[0], Postgres uses sscanf with %x. %x can wraparound. This means SELECT '10000000aa:bb:cc:dd:ee:ff'::macaddr; will return aa:bb:cc:dd:ee:ff. 1) When parsing a tid[1], Postgres uses strtoul. The return value of strtoul is different across platform for the empty string. This means on some platforms Postgres SELECT '(,5)'::tid; will error and others will accept it. 2) Postgres missed an overflow check in it's cash type[2]. When running SELECT '-92233720368547758.08'::money / (-1)::int8; some platforms will error and other's will return the MIN value. Postgres does check for this for some of the other cash related functions, but it missed it for one of them. 3) When hashing the "char" type Postgres will cast a char to an integer[3]. On some platforms char is signed and on others it's unsigned. This means the hash of a char can be different depending on the platform. If you are using a hash index or hash partitioning on a char and move your DB from x86 to arm, the hashes will differ and your index/partitioned tables become corrupted. Note that this is special char type that you have to refer to by "char" that is separate from the typically used CHAR(n) type which is what you typically use, hence this would never come up under real usage. The common pattern with all of these is they rely on C behavior that differs across platform (integer overflow, char signedness, strtoul). Rust is better about having more consistent behavior across platforms so these cases get flagged when the Rust code and the C code differ. [0] https://github.com/postgres/postgres/blob/REL_18_3/src/backend/utils/adt/mac.c#L71-L81 https://github.com/postgres/postgres/blob/REL_18_3/src/backe... [1] https://github.com/postgres/postgres/blob/REL_18_3/src/backend/utils/adt/tid.c#L75-L81 https://github.com/postgres/postgres/blob/REL_18_3/src/backe... [2] https://github.com/postgres/postgres/blob/REL_18_3/src/backend/utils/adt/cash.c#L155-L165 https://github.com/postgres/postgres/blob/REL_18_3/src/backe... [3] https://github.com/postgres/postgres/blob/REL_18_3/src/backend/access/hash/hashfunc.c#L47-L51 https://github.com/postgres/postgres/blob/REL_18_3/src/backe...

appplication 2mo ago
Very cool project and good finds. What do you see as the end state for your project - do you think pg has a path to upstream, or would this be a fork? Without knowing anything about the pg team, I would assume they would be hesitant to even consider an under the hood switch, just from a risk management perspective, regardless of test coverage and formal verification. But I could be wrong.
- malisper 2mo ago
  Thank you for the kind words! My goal is to build the best database possible. I'm trying to imagine what Postgres would be like if it were built today. I've been able to make a bunch of big architectural changes that the Postgres team has been talking about but hasn't yet made. For example, threads instead of processes and a vectorized executor. I think everyone would agree the types of changes I'm making are good ones. The challenge Postgres faces is there's millions and millions of Postgres databases out there so they are focused on minimizing the risk of breaking any existing functionality over doing a big high risk rearchitecture. I could see ideas from what I'm doing gradually making their way into Postgres, but I think the odds that pgrust (or any Rust code for that matter) gets merged into Postgres is close to zero.
  - wonger_ 2mo ago
    For other interested spectators, I found this post by the author to be a good example of architectural changes in pgrust (along with motivations): https://malisper.me/the-four-horsemen-behind-thousands-of-postgres-outages/ https://malisper.me/the-four-horsemen-behind-thousands-of-po...
throwaw12 2mo ago
these are impressive findings, I am curious what was your process to convert existing code to formal verification languages like TLA+. My basic understanding was to verify high level abstractions (e.g. transport ACK, fsyncs and so on), but verifying this deep probably requires complete verification of stdlib methods used by Postgres, otherwise how can you pinpoint culprit is the sscanf?