joerichey

If you accept that _all_ vector spaces have a (Hamel) basis, you can then prove the Axiom of Choice: http://www.math.lsa.umich.edu/~ablass/bases-AC.pdf

This means if you want to deny the Axiom in some cases, you will also have to allow for the existence of vector spaces without a basis.

One thing that makes Secure Boot nice is how it (in theory) works _with_ measured boot. You get a measurement into the TPM that contains the public signing key that was used to verify the signature on your bootloader. This means if you update from one signed bootloader to a newer signed bootloader, you don't need to change any disk encryption or sealing.

Of course blocking execution is orthogonal to verifying the boot chain, but unfortunately those issues are conflated in the UEFI spec.

Part of the issue with this MSI problem, is that the firmware also measures TPM events that say "Secure Boot is enabled with this configuration" even when it's not. These events are (almost always) used for FDE (via PCR 7) with a TPM.

This means that even if you setup FDE correctly (binding to say PCRs 0, 7, and 11), you would be able to bypass FDE using this MSI bug. For example, BitLocker binds to PCR 7.

You could get around this bug by sealing to PCR 4 (which contains the _hash_ of the bootloader). But then you have to redo FDE sealing every time your bootloader updates.

I looked into this on my motherboard, and the issue is that MSI's firmware measures in the TPM events saying "Secure Boot is On", even when it is in this insecure mode.

This means that even if Windows "checks" (via measured boot) that Secure Boot is on, they are still being lied to by the motherboard firmware.

Whoops! You're right, instead of "successor" I should have just said "newer".

This is actually what the Precision Time Protocol (PTP) does. It's the successor to NTP, so it improves on some of NTP's mistakes. The protocol uses TAI, but also sends the TAI-UTC offset so the computer can display times in UTC.

https://en.wikipedia.org/wiki/Precision_Time_Protocol

For future leap seconds, Google (including GCP) are planning to use a "standard" smear (https://developers.google.com/time/smear). This is also the same smear used by AWS.

It seems like if the ITU decides to keep the leap second (a bad idea, in my opinion), the large infrastructure providers will just use the same standard smear for their clocks.

One reasonable way to do this could involve running the reference TPM2 simulator [0] on the Arduino. It's just a C library that already implements all the cryptographic routines and TPM2 commands. In fact, this is basically how TPM vendors implement their chips. They just generally have:

  - A lot more hardening against physical attacks
  - Cryptographic libraries optimized for their low-resource hardware
  - (sometimes) a vendor certificate for a primary TPM key, aka an "EK cert"

Certainly a TPM running on an Arduino wouldn't have the physical hardware properties of a "real" TPM. But you could probably get it into a state with similar software properties.

[0] https://github.com/microsoft/ms-tpm-20-ref

As someone who's spent too much time with this stuff, you're correct. The TPM (either 1.2 or 2.0) is an entirely _passive_ chip. It only creates keys or measures data if the OS or UEFI asks it to. This means that it can't block or modify programs on your CPU.

Secure Boot is implemented by UEFI, so it can block the loading of a particular bootloader. You can have Secure Boot without a TPM or have a TPM without Secure Boot. They can be useful together though as you can have a disk-encryption key with a policy saying "I can only decrypt stuff if you've booted using Secure Boot in a particular configuration".

As for DRM, the TPM doesn't work very well as part of a DRM solution (as it's entirely passive). This is probably why very few (if any) DRM products use TPM. Most PC DRM that I've heard of either uses Windows Kernel modules or Intel SGX.

I don't think that Windows 11 requires any sort of EK cert at all. If they did, it would require them to restrict the TPMs to a list of "approved" vendors.

In this case, they bought the actual TPM2 part of the chip from Infinion, so it might already have an EK Cert on it.

Shouldn't this be marked with (2014) as it was made at DebConf 14?

For point (2), Google did open source Bazel https://bazel.build/ which is essentially just the internal build system Blaze.

(Google employee here)

If the change is small or can be automated (i.e. changing # of parameters or function names), we run a script to make the change over the entire monorepo. This enormous CL is then approved by one of the Global owners.

If the change is complex (or non-obvious), you generally introduce the new API in one CL, change each use manually (say one CL per team), and then remove the old API in a final CL. In that case, you need each team to sign off. This isn't too hard in practice, teams are generally expected to approve cleanups.

Personally, I would use an explicit non-commercial license in this case. WTFPL isn't a real license (and isn't considered open-source by OSI).

Things like the AGPL and CC-BY-NC-* are actually written by lawyers and make it clear what you actually want.

> If a Google employee in their free time contributes to an AGPL project, that employee needs to open source all IP related to their contribution to the project.

This isn't the problem. The reason for contribution bans is stated in [1]:

"Our general philosophy is that we do not allow patches to projects that Google cannot use."

[1]: https://opensource.google/docs/patching/#forbidden

So the issue isn't in-work hours vs off-work hours (as that line is fuzzy), but who owns the copyright.

The above link [1] is for the automatic process where Google still owns the copyright (hence no AGPL or non-Commercial stuff). This works for 99% of stuff and is easy.

There's a second process called IARC [2] which lets the employee retain the copyright. It's not automatic but allows for AGPL, non-commercial, or proprietary contributions.

We also have a few AGPL projects that were whitelisted due to COVID-19 [3].

[1]: https://opensource.google/docs/patching/ [2]: https://opensource.google/docs/iarc/ [3]: https://opensource.google/docs/patching/#no-review

At Google, MPL (and other copyleft licenses) are OK for internal use and for external contributions.

I think we have a mirroring system setup to automatically publish any internal changes.

Edit: See https://opensource.google/docs/thirdparty/licenses/#reciproc... for the public info about mirroring.

As a current Google employee, the OSS contribution process has gotten way better. Basically, anything that is BSD/MIT/Apache/LGPL/GPL/EPL/MPL no longer needs approval.

AGPL and the non-commercial licenses are still banned.

Edit: The Google OSS contribution guidelines are actually public, if anyone wants to take a look: https://opensource.google/docs/patching/

I think you would actually need Box<dyn Foo>. But the bigger point is that the current build system can't figure out that a rebuild isn't necessary in these cases.

If you're working on safety-citical software, I think using formally verified C code (as discussed in the article) would be the best approch.

If a bug could kill someone, you should (to the greatest extent possible) have a proof that such bugs are impossible.

Take a look at the dep[1] tool. It allows you to ship your project with all of its dependencies included. This means that only your source is needed to build your application/package.

The Gopkg.toml/Gopkg.lock files in dep are quite similar to Rust's Cargo.toml/Cargo.lock files. I think it's a good move as Rust has probably the best package management story out there.

Also, as the other comment mentioned, github.com is not "special" in any way. Any website with a git repo will work just as well. In fact, some key libraries are served from golang.org/x/<whatever>[2] not github.com.

[1]https://github.com/golang/dep [2]https://github.com/golang/go/wiki/SubRepositories