Agree. I don't read it every week, but I greatly appreciate the quality (both of the technical content and the lack of advertising/sensationalism/clickbait) when I do read an article. Happy to pay to support this style of tech reporting and journalism.
This reminded me that I'd let my LWN subscription lapse after a credit card expired. Just renewed for a year and turned on automatic renewals (at least until the next credit card expiration).
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.
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.
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.
I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload. The docs tend to say "same hardware architecture". Though if they don't intend to support this case I think it's a shame if the pg_control checks allow the server to start after such a migration.
> I think the postgresql maintainers don't claim to support moving a database from x86 to arm without a dump-and-reload
I would be very surprised by that because that means replicating a database between the two platforms would lead to corruption.
btw, this bug breaks dump-and-reload too. If you use partitioning, each partition is dumped and restored individually. In this case though, you'll get an error when you try to restore the data because it's trying to put data in the wrong partition. That's better corruption, but still an issue.
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?
Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of
GOTO is back ! So glad to see CBMC used. I used to write translators to GOTO for simple code checking and was wondering where the recent state of the art was. Thanks for the pointers.
Did you have a look at why3 and generating verification conditions from Rust or C code (as frama-c does) ?
Interesting. I am still defaulting to ChatGPT when I anticipate having a multi-turn conversation.
But for questions where I expect a single response to do, Google has taken over.
Here's an example from this morning:
It's my first autumn in a new house, and my boiler (forced hot water heating) kicked on for the first time. The kickboards in the kitchen have Quiet-One Kickspace brand radiators with electric fans. I wanted to know what controls these fans (are they wired to the thermostat, detect radiator temp, etc?)
I searched "When does a quiet-one kickspace heater turn on". Google Overview answered correctly [1] in <1 second. Tried the same prompt to ChatGPT. Took 17 seconds to get the full (also correct, and similarly detailed) answer.
Both answers were equally detailed and of similar length.
[1] Confirmed correct by observing the operation of the unit.
The bindings should also work with tinygo's compiler if you're careful with deadlocks (see docs/ERRATA.md).
Haven't tested the typecasting that's required for the components yet though, they might break because of some generics quirks (e.g. Wrap/Unwrap helper methods).
Working on Fraim, open-source agents for cloudsec and appsec engineers to complement existing deterministic scanners. Born out of our 3 years of learnings building such scanners for IaC. Turns out in the real world policies are subjective enough to make this hard.
Examples:
- Policies are frequently subjective. Hard to codify, but LLMs can evaluate them more like a security engineer would. "IAM policies should use least privilege." What is "least" enough? "Admin ports shouldn't be exposed to the Internet." What's an admin port?
- Security engineers are stretched thin. LLMs can watch PRs for potentially risky changes that need closer human review. "PR loosens authz/authn." "PR changes network perimeter configuration."
- Traditional check runs (SAST, IaC, etc.) flood PRs with findings. Security doesn't have time to review them all. Devs tends to ignore them. Frequent false positives. LLMs can draw attention to the important ones. "If the findings are unusual for this repo, require the author to acknowledge the risk before merging."
reply