Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What can you confidently guarantee about your software?

queue.acm.org

Post reply on HN
Print view View original

31–40 of 71 posts

Re: What can you confidently guarantee about your software?

#31

Post by dfabulich »

win311fwg wrote: post #29
dfabulich wrote: post #28

Earlier quoted context omitted.

The rules of email validation are not remotely well defined! Syntactic email validation is an impossibly hard problem. https://www.netmeister.org/blog/email.html IMO the industry consensus is never to "validate" email addresses syntactically, but simply to ensure that the email address contains at least one @ and to verify the email address by emailing it an activation code. Proofs would not have uncovered these fail…

> The rules of email validation are not remotely well defined! RFC 5322 fully defines the structure. > IMO the industry consensus is never to "validate" email addresses syntactically That is true, but not because it isn't well defined, but because it is hard to get right. Keep in mind that most developers don't even know what a property-based test is, and of those that do, only a small subset of them know how to use…

Don't forget RFC 5321! But the RFCs are ignored in practice by all popular mail servers. There are email addresses that work in practice that don't comply with the RFCs, and there are email addresses that the RFCs permit that don't work in practice.

(This happens with a lot of standards; sometimes people just ignore them and do their own thing. Something similar has happened with SVGs.)

If you write a formal verification of a syntactical email validator that ensures that all/only RFC-compliant email addresses are valid, you'll have completely wasted your time. Don't do it. Just check for at least one @ sign, and email the address to test it.

(This is a perfect example of the trap of formal verification.)

Re: What can you confidently guarantee about your software?

#32

Post by TacticalCoder »

dfabulich wrote: post #17
gf000 wrote: post #8

Earlier quoted context omitted.

Well, I'm someone who barely knows more than jack about formal verification, but in pretty much every case you have to have some kind of model that you are actually verifying. How close that model sits to the real thing you have modeled is an important question, and you are free to be as close or distant as you want -- e.g. for verifying different properties of a programming language you might decide to not care abou…

Formal verification is a siren song. The siren sings, "bug-free code is possible in principle!" But it's a trap. Even with LLMs, bug-free code is impractical. I argued that property-based testing is mostly unhelpful for e-commerce/CRUD apps, and that formal verification is a performance improvement on property-based tests. In a property-based test, you identify some rule (an invariant) that you want to apply to your…

> It's already useful for many software platforms. It's useful for databases, where reliability is essential. It's useful for parsers, particularly when you expect the end user to be attempting to send you hostile code.

> But e-commerce apps?

So the e-commerce app doesn't use a DB?

And the e-commerce app receives zero user input that needs to be parser so doesn't use any parser either?

If you say its useful for, for example, DB and parsers, then any app using these benefits from it.

Re: What can you confidently guarantee about your software?

#33

Post by Analemma_ »

win311fwg wrote: post #29
dfabulich wrote: post #28

Earlier quoted context omitted.

The rules of email validation are not remotely well defined! Syntactic email validation is an impossibly hard problem. https://www.netmeister.org/blog/email.html IMO the industry consensus is never to "validate" email addresses syntactically, but simply to ensure that the email address contains at least one @ and to verify the email address by emailing it an activation code. Proofs would not have uncovered these fail…

> The rules of email validation are not remotely well defined! RFC 5322 fully defines the structure. > IMO the industry consensus is never to "validate" email addresses syntactically That is true, but not because it isn't well defined, but because it is hard to get right. Keep in mind that most developers don't even know what a property-based test is, and of those that do, only a small subset of them know how to use…

I'm speaking from painful experience here: if you assume RFC 5322 has anything whatsoever to do with how email addresses actually work in the wild, you're in for a world of hurt. Popular email providers don't give a shit what RFC 5322 says, and you can't either if you want to have any hope of actually sending and receiving mail. Test messages are the only way to validate an email address, period.

Re: What can you confidently guarantee about your software?

#34

Post by jongjong »

"The proof was only as good as the spec." Is the sentence which will go on the tombstone of Formal Verification.

The spec has always been the problem. Whether the flaws in the spec arise from the customer or from the developer filling in the gaps in the spec incorrectly.

If I built an entire system and the spec does not mention access control logic, then formal verification will neither prove nor disprove that the software is secure. It's just not in the spec...

You have to know exactly what security properties you want. By the time you've written them down succinctly and correctly as a spec, you might as well have written them down succinctly and correctly as code.

The spec has to be just as detailed and will be just as error-prone as the code itself.

Re: What can you confidently guarantee about your software?

#35

Post by win311fwg »

dfabulich wrote: post #31
win311fwg wrote: post #29

Earlier quoted context omitted.

> The rules of email validation are not remotely well defined! RFC 5322 fully defines the structure. > IMO the industry consensus is never to "validate" email addresses syntactically That is true, but not because it isn't well defined, but because it is hard to get right. Keep in mind that most developers don't even know what a property-based test is, and of those that do, only a small subset of them know how to use…

Don't forget RFC 5321! But the RFCs are ignored in practice by all popular mail servers. There are email addresses that work in practice that don't comply with the RFCs, and there are email addresses that the RFCs permit that don't work in practice. (This happens with a lot of standards; sometimes people just ignore them and do their own thing. Something similar has happened with SVGs.) If you write a formal verifica…

> Don't forget RFC 5321!

As long as you don't forget RFC 6531.

> But the RFCs are ignored in practice by all popular mail servers.

While I agree that you can make a compelling case that sending email is the C in CRUD, usually when someone is talking about CRUD they are referring to systems that satisfy all four letters. U violates the spirit of email, and R and D is usually handled independently of the MTA. So what email servers do here is irrelevant. If you go way back up the comment chain you will even see that Postgres was specifically mentioned. Postgres doesn't care what an email server does, but it does care about data consistency.

> Just check for at least one @ sign

That's a valid specification and in practice you are going to want to make that a PBT to ensure that your implementation actually adheres to the specification. You might try testing foo@bar.com, but what about foo\u0040bar.com? Will you think to test it too? Probably not. Will your code handle it correctly? You may be perfect, but when we get out into the general developer population where all kinds of crazy things show up when they start monkeying with your code, the answer is also probably not.

Looking simple isn’t a reason to not use the tools at your disposal, even if many won’t.

> and email the address to test it.

Poor general advice. That is expressly illegal in some jurisdictions.

Re: What can you confidently guarantee about your software?

#36

Post by [deleted] »

Analemma_ wrote: post #33
win311fwg wrote: post #29

Earlier quoted context omitted.

> The rules of email validation are not remotely well defined! RFC 5322 fully defines the structure. > IMO the industry consensus is never to "validate" email addresses syntactically That is true, but not because it isn't well defined, but because it is hard to get right. Keep in mind that most developers don't even know what a property-based test is, and of those that do, only a small subset of them know how to use…

I'm speaking from painful experience here: if you assume RFC 5322 has anything whatsoever to do with how email addresses actually work in the wild, you're in for a world of hurt. Popular email providers don't give a shit what RFC 5322 says, and you can't either if you want to have any hope of actually sending and receiving mail. Test messages are the only way to validate an email address, period.

[deleted]

Re: What can you confidently guarantee about your software?

#37

Post by aezart »

toast0 wrote: post #9
dfabulich wrote: post #2

Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…

The first part of formal verification is getting a formal specification. I don't know about most developers, but I rarely get a written specification for anything I work on, and when I do, it's no where near what would be needed to turn it into a formal specification. Anyway, the specification is subject to change at the whim of a hat, so putting a lot of effort into verifying it is foolish. I do see value in formal…

What we get typically is a second or third-hand summary of an analysis someone else did about how the current version works, with no indication of what stuff has to stay as-is in our replacement and what stuff can be improved.

Re: What can you confidently guarantee about your software?

#38

Post by calf »

dfabulich wrote: post #2

Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…

I don't understand your argument, why precisely is contemporary app development thought to be so simple that it is not even worth thorough property testing, let alone FV? Isn't that attitude (on the part of the industry as a whole) a type of self-fulfilling prophecy?

Re: What can you confidently guarantee about your software?

#39

Post by toast0 »

derdi wrote: post #25
toast0 wrote: post #9

Earlier quoted context omitted.

The first part of formal verification is getting a formal specification. I don't know about most developers, but I rarely get a written specification for anything I work on, and when I do, it's no where near what would be needed to turn it into a formal specification. Anyway, the specification is subject to change at the whim of a hat, so putting a lot of effort into verifying it is foolish. I do see value in formal…

Nitpick: You don't necessarily need any specification at all in order to reap benefits. Formal verification languages come with a lot of conditions that your program must fulfill in order to be accepted: Every loop terminates, every object you want to read/write is non-null, every list or array access is in bounds, etc. For example, if you load an arbitrary C program into Frama-C, you'll have tons of properties to pr…

> The promises you get is that the program will always terminate

I don't want my programs to terminate though.

Re: What can you confidently guarantee about your software?

#40

Post by agentultra »

dfabulich wrote: post #2

Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…

If you are willing to relax the restrictions, and you probably should, model checking is probably worth its weight in gold for these scenarios.

You won’t get proofs but you will spell out your logic in a formal language[0] and each run of the checker will exhaustively check your invariants[1].

[0] Useful because often you will learn something you hadn’t considered.

[1] A proof will guarantee your statements hold over quantifiers that are much too large for a model checker to check exhaustively. But, you can say that for a model of size N, property Y is guaranteed to hold. The “small model theorem,” posits that if there is an error in your specification, it is more likely to show up in a small model. You sacrifice the completeness of proofs but this trade-off has been worth it to me.

Post reply on HN