_vdpp

Doxygen can generate similar diagrams with C/C++ code: http://doxygen.nl/ At a former employer, we made it part of the CI pipeline and the class hierarchy diagrams and call diagrams were great for newcomers to get oriented with the codebase.

Here's a formally-verified DNS Server: https://ironsides.martincarlisle.com/

Not all the way down to the instruction level, but it's a start.

Flow analysis and SMT solvers are mathematically-sound, so if done correctly, a fuzzer would have no luck finding a path through the code where any undefined behavior (or behavior that violates the contracts you've specified) could take place.

Getting started with SPARK, you'll see messages like "Can't prove that this variable won't overflow" (usually with corner cases like "when x = 4,294,967,295 and y = -1"). So it kind of makes you realize how error-prone code can be.

A statement like "x++" has the assumption baked into it that x isn't going to be INT_MAX. Fuzzers work by manipulating your control flow such that x _will_ be INT_MAX and cause an overflow or other bad stuff. Formal verification exposes all those assumptions and when people complain about slow development, it's because you're basically making the code "fuzzer-proof".

"Hacker-proof" is hyperbole, but not as much as some might have you believe. People have pointed out that the specification has to be correct. My code in the pastebin proves every element in the output array is even, but if the code is supposed to produce an array of odd numbers, then obviously that's still a bug, even though it's been "formally verified".

I wouldn't use the term "hacker-proof", but I would say "hacker-resistant". FV _can_ eliminate whole classes of vulnerabilities that attackers could otherwise use. A common trope is "well there's still hardware bugs or the spec could be wrong, so why bother?" I mean, sure, a hacker could cut the power to the datacenter, too, but IMO that's not a reason to ignore tools that can make the software we write much more robust.

One issue that can crop up is that you can't always prove what you're trying to specify. The state space can grow too big and the solver can't figure it out in a timely fashion, so you have to make assumptions and hope your tests give you enough confidence to deploy the system. This is basically the halting problem - it doesn't say that it's impossible to prove termination (or any other property) of some code, it just says that you can't _always_ prove them.

nVidia recently began using SPARK in some of their work, the video does a good job explaining some of the bugs that FV eliminates: https://www.youtube.com/watch?v=DZSSyWlsb28

Short version: Write algorithms using mathematically-sound logic whose correctness and properties can be _proven_ the way you might prove the correctness of a math formula.

Long version: Formal verification is a broad topic with a lot of different facets. But hopefully this sheds some light on some of the more useful ones:

Model-checkers like TLA+. You can specify an algorithm, say something simple like a bank account transfer where a sender's account is debited, and a receiver's account is credited. You can then set constraints, such that the sender's account must have enough to cover the transfer, etc. TLA+ will then run through all the scenarios in your algorithm to find corner-cases when the constraints aren't met. It's useful for modeling distributed systems, and you can try simulating an algorithm in parallel to see error conditions in multi-threaded code.

The downside to TLA+ is that you produce a specification, but still have to reproduce the specification in compilable/runnable code. I understand Amazon has had a lot of success using TLA+ to wring out potential bugs in systems before implementing them, and Leslie Lamport (author of TLA+ and creator of LaTeX, too) has some great (and entertaining) videos on his website explaining how they work: https://lamport.azurewebsites.net/tla/tla.html

There are formally-verifiable dialects of programming languages like the SPARK dialect of Ada, and Frama-C, which let you specify pre and post-conditions for functions, and then it will perform model-checking with flow analysis and SMT solvers to ensure those conditions are met in a way that's mathematically sound. Some conditions, like lack of buffer or integer overflows, are always checked. This way, code which has passed the proof stage can truly be said to be free of run-time errors, and whatever extra contracts you've added in your code will be met as well. Since all of this is checked at compile/proof-time, there's no run-time penalty for the extra assurance.

I came up with this simple example of SPARK code that proves if I have a function that doubles every element in an array, then the result satisfies a contract where every element in the output is even: https://pastebin.com/BtkaEDQ5

There are also proof assistants and theorem proving tools/languages like HOL, Isabelle, Coq, LEAN, and others which IMO fall under the umbrella of formal verification, but more on the computer science side than software engineering. In contrast, TLA+ and SPARK are very useful and practical for developing high-integrity software. Still, they're programming languages, and you can write executable code in them that can be said to be mathematically sound. A good resource is the Software Foundations course: https://softwarefoundations.cis.upenn.edu/

Some dependently-typed programming languages like Idris, F*, Dafny, and (I think) Liquid Haskell provide different mixes of these capabilities, but are geared towards producing usable software.

That's helpful, thank you.

Using a flat-file based system appeals to me, but one question I've never had a good answer for is at what sort of scale does a certain database make sense?

Aside from questions of ACID, I get the idea that a lot of people jump to databases because they're uncomfortable with file operations, frankly. But obviously they make sense for other use cases - what is the decision matrix? Just a gut feeling?

Even worse, assuming the high-grade brand is better to begin with - are you buying the real thing, or a counterfeit?

If your target audience is investors, instead of end users.

The article mentions a mine in Afghanistan as a source of the best Lapis Lazuli, but I believe in ancient Egypt (and probably the Classical era), it was the _only_ source.

There are some really interesting documentaries about the mine, and what impresses me most is just how remote and dangerous the trek is. Mining there 4000-5000 years ago with primitive tools, and the journey required to get the Lapis from Afghanistan all the way to Egypt is really very remarkable. It's a difficult journey today even with Range Rovers.

Related to the OP, but not Lapis mining: an interesting related discovery (2009): https://chemistry.oregonstate.edu/content/story-yinmn-blue

It's probably a lot more accessible than you think.

The congressional recommendation is for entrance into the US Air Force Academy, which is a 4-year university.

If you already have your degree, you can apply for OTS (which is your initial officer training - I think it's 3 months long now) and a pilot slot directly.

Another option a lot of people overlook too is getting to pilot training via the Reserves or ANG. Those units can interview and hire you directly, and you'll go through the same training and do the same job with a lot less red tape.

True - but a lot of people self-disqualify because of rumors and urban legends. Make them tell you "no" if it's something you want. There are waivers for many medical issues, but if you don't ask you'll never get one.

I was working as a SWE for a large defense contractor on some pretty neat projects, and I felt like I was good at what I did. It was 40 hour weeks, good benefits, good pay, but I was bored and miserable. I lived in a town with no friends, and was so desperate for a change and some adventure, that I left the industry to join the military.

I took what I call a 12 year sabbatical from tech. I became an officer, went to pilot training, learned lots of new and useful skills, met lots of very good and interesting people, some of whom are my best friends.

Taking off from a short airfield in a blizzard, at night, wearing NVGs is an experience I don't care to re-live, but I'm glad I have something to talk about at parties.

A quote that affected me greatly during the time I was thinking about leaving: "if somebody wrote a book about your life, would anybody want to read it?"

After getting married (to somebody I met during one of my training courses), settling down, and having kids, a quieter, 40-hour-a-week lifestyle started to sound pretty good again. I had always been a hacker at heart, and realized that I was getting to the age where it was probably now-or-never if I wanted to re-enter the industry. So I went back into tech! It's better the 2nd time around.

Zero regrets.

There's a lot of FUD going on. You're correct in that _many_ speculative execution attacks in general are very difficult to exploit in a useful way. I.e. things like timing side-channels using shared TLDs or in a hyper-threaded core.

The Meltdown attack (also a speculative execution attack) is a much bigger deal - it's easy to exploit, and an attacker could basically read arbitrary memory on your system. It is easier to mitigate, too, with KPTI. Before KPTI, your OS kept the full set of kernel page tables mapped when user processes are running, the contents of which could be exfiltrated using the speculative execution side-channel.

AMD processors (and I believe newer Intel processors) are basically immune to Meltdown, so it may be safe for you to turn off KPTI for a (minor) performance boost. Having said that, newer CPU TLBs have process-context IDs that let the OS make up for some of the performance impact, so you might not notice a difference at all.

The original "Spectre" attack (name in the whitepaper - not to be confused with the greater class of Spectre attacks) allowed out-of-bounds memory access within a process' address space via speculative execution. So, if your browser was running in a single process, then some Javascript could read other browser memory containing things like passwords, keys, etc. If your browser is running scripts or pages in their own sandboxed process, then the risk is pretty low.

Any Spectre mitigations performed by the kernel are not going to be a silver bullet, anyhow. These are _mitigations_, not "magic Spectre attack prevention" features. Unless out-of-order execution (or caches!) is eliminated entirely, speculative execution attacks are going to be a threat. (Interestingly, Itanium CPUs and it's VLIW architecture appears to be immune to these attacks.)

Even compiling your software with Spectre mitigations turned on (available in MSVC, not sure if GCC has implemented it yet) doesn't do a whole lot of magic - it will insert a serializing instruction (LFENCE on x86-64) to clear out the pipeline during certain loop-branch combinations, ensuring that a speculative read can't occur before the outcome of the branch is decided.

Any time there are shared resources between processes, CPUs, computers, datacenters, etc. there is a side-channel - period. What can be leaked via this side-channel, how noisy the side-channel is, what the rate of data exfiltration is, these are things under our control, but eliminating side-channels entirely is a fool's errand.

So, would I risk turning off the Spectre mitigations? I'll put it this way: I'd worry about the Spectre kernel flags after I had a Linux antivirus program installed, and turned on and tightened up my AppArmor or SELinux configs.

I'm sure many of the people crying out against the crime of disabling Spectre mitigations haven't done that yet (just like I haven't) - because it's a PITA! So, if you disable the mitigations and decide the performance increase is worth the risk, I wouldn't fault you for it.

The whole reason these exploits exist in the first place is because the CPU performance increases available with speculative execution, out-of-order execution, deep CPU pipelines was worth the risk (to their reputation, at least). I don't see a lot of people going back to buy Itaniums because they're worried about Spectre attacks.

Now - would I turn off KPTI? On an AMD CPU, sure. On Intel (unless you've double checked, the CPU was produced in the last couple of years, and it's immune to Meltdown) - ABSOLUTELY NOT!

Reducing timer resolution was done early on as a quick reaction by browser developers when Spectre & Meltdown were first publicized.

All an attacker needs to do is distinguish between a cached and non-cached memory read - i.e., was accessing some variable "faster" or "slower". There are lots and lots of ways to measure this. A good whitepaper is "Fantastic Timers and Where to Find Them: High-Resolution Microarchitectural Attacks in Javascript".

The TLDR is that timer resolution reduction is ineffective as a speculative attack mitigation.

By his definition, isn't a "talk" skeuomorphic as well?

That's a nice way to look at it. Like the GP, I almost never return to bookmarks.

Endpoint supervising isn't always an option. As more IoT devices start to use TLS connections to phone home, a network MITM may be the only way to see what they're reporting. Breaking TLS isn't just something that Big Brother would want to do.

(This is assuming they aren't using pinned certs baked into their firmware, anyhow. I don't have good data on which manufacturers/devices are doing this, but somebody else might know.)

I think you're talking about "The SQLite Amalgamation" - https://www.sqlite.org/amalgamation.html. I hadn't heard of it before, so thanks for encouraging me to look it up - seems like it might come in handy!

I'd have to assume so - it was plain to see.

I hadn't heard about rosin fumes being dangerous until this thread. I'll definitely have to learn more and work on some better ventilation in the future. I do love that smell though!

I never heeded much caution when soldering using lead solder growing up. When I got to university, the department employed a long-time soldering professional, with NASA certifications, etc. She was very knowledgeable, but visibly suffered from what I assumed was chronic heavy metal poisoning - hair loss and visible skin problems. It was a pretty big wake up call for me that I needed to treat solder with more caution.

Especially for people introducing children to electronics, make sure you're using lead-free materials. If for whatever reason lead is unavoidable in a project, make sure you're using good ventilation and wash thoroughly before going around your kids after you've handled lead.

VB the _language_ obviously has its limitations and frustrations, but VB the _tool_ will be missed. It seems like every alternative mentioned here adds a lot of additional friction for writing simple, one-off utilities.

I don't always want to dink around with the Visual Studio installer to make sure the right version of the MSVC or .NET libraries are installed, or fiddle with code to get a GUI layout to look nice, etc.

Having the IDE, compiler and GUI designer in one big coherent monolith had its advantages.

You might want to look at the Why3 meta-solver framework. It uses an intermediate language, Why3ML, that can be run against an array of different SMT solvers, including Z3 and CVC4. If you run into something that SMT can't figure out in a reasonable time-frame, you can use Coq to manually-prove your theorems too.

Languages like SPARK and Frama C generate Why3ML as an intermediate output that then gets transformed to run against whatever solvers are available during the verification phase of development. Since the verification/proof phase is separate from compilation, you can write your code with fewer checks initially, and then add conditions as you go to prove functional correctness.

I'd be surprised if C++ is ever touted seriously as a language suited for formal verification. I think the language just has too many corners and escape hatches to be able to nail down its semantics in a way that automated provers can handle.

Having said that though, I'm pretty sure the MSVC Driver Verifier tool uses an SMT solver to try and prove the absence of certain types of errors, so who knows?

My understanding is that there's still VM, but it uses a separate buffer (on-chip memory map) containing a list of segments that map each part of the process' memory to a physical address (virt->physical offset + length), rather than a multi-tiered paging structure. The advantage is quick virtual -> physical address translation and less space used for them vs page tables, but the downside, as you point out, is what to do when a process exceeds it's initial heap or stack segment.

In this case, I think the Forwardcom solution is to add another entry in the memory map for the next 2*n bytes of heap space.

I recently used Ada (not the SPARK subset) to develop an assembler/simulator (for a made-up ISA) for a computer architecture course I was taking. I used the GtkAda bindings for the GUI, which worked well: https://github.com/docandrew/YOTROC

I'm using SPARK for another project, and I think it's great. I don't think there is really an easier way of writing formally-verified software right now. Depending on the pre-conditions and post-conditions you put on your code, it can offer much stronger guarantees than other general-purpose programming languages do, but _proving_ those guarantees can be tricky if you don't have much experience with it.

The nice thing about SPARK is that if you get something you can't prove (either because it's not legal SPARK or because the solver can't figure it out), you can turn off SPARK mode on a per-function or per-package basis and either come back to it later, or just prove that callers to the function abide by the specification without the function body itself being legal SPARK.

For IDEs, I prefer VSCode over AdaCore's GPS IDE; AdaCore has a VSCode LSP plugin that I use: https://github.com/AdaCore/ada_language_server. Having said that, I used the GPS IDE for the computer architecture project and it worked well.

Good luck!

I think the article created a lot of the confusion. Having access to cleared people is important to companies primarily for winning lucrative government contracts. For example, if a 3 letter agency wants to implement a cloud service on an air-gapped intranet, or award a contract to implement social-media algorithms to suss out terrorist networks, they'll look to companies with that sort of expertise. But if those companies don't have a corps of cleared employees, they're out of the running. Having said that, having trustworthy employees (which a clearance implies, but does not guarantee) might be valuable to companies not dealing with classified information, but the article left out the real reason that companies are heavily invested in recruiting people with clearances.