coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Sam Kuper <sampablokuper AT posteo.net>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A verified bootstrapping computer (academic curiousity)
- Date: Sat, 8 Jan 2022 23:18:39 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sampablokuper AT posteo.net; spf=Pass smtp.mailfrom=sampablokuper AT posteo.net; spf=None smtp.helo=postmaster AT mout01.posteo.de
- Ironport-data: A9a23:IPLUq6xXlkCu11IPe/h6t+dmxyrEfRIJ4+MujC/XYbTApDIrhT1WzjBJDG7QMq2IYWemLt4iPo609U9QvsSAnNRjOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA/3z27AsFehsJpPnjkrrYuiJQUVUj/nSHOKlUL6cYEideCc9IMsfoUI78wIGqtUw6TSJK1vlVeLa+6UzCnf9s9JHGj58B5a4lf9alK+aVAX0EbAJTasjUFf2zxH5BX+ETE27ByOQroJ8RoZWSwtfpYxV8F81/z91Yj+kurP8b1FSG/jKOhOSh30QV6XKbhpq/3xvlPhkcqFCLxkK49mKt4gZJNFlrpW1UQ4jOqrPhfwQSTFAFDpiMKoA/rLbSZS6mZbLkxaYKSSEL/JGVR5nZtVCpI6bG1pm/vsBbTsJcxqrnPOz2Lv9S+92h81lItODAW+1kmU4mGqfUOJ/FMiFG7GQsIcehmpu2NQVSK6YOt5GPBNxSj/FRTFPHnYeLq4kuvPx3iynN2RMwL6Oja8w/nSLlUpp16PxPd2TdtHieCmcpW7AzkquwogzKkhy2B2jJTu5HraEg+jSgXuiHpoVD6G18bhmjTV/A0R75AI+DTOGTTuR0yZSmO6z72QM/TEyoK908kG3JjU4dwPtu2aK53bwRPIJe9DXK2ixJm78+wGCGmUDCDhMdLTKcedeqSMCjje0oj8iOdCjXHB5h55QGnd4YA5e4RQoEFI=
- Ironport-hdrordr: A9a23:GeHZ3q1tySuXicDPbm7NsAqjBI0kLtp133Aq2lEZdPVwSL3+qynOpoV+6faQslwssR4b9exoVJPufZqYz+8S3WBzB8bGYCDDsGusaK5l6I7l3SH4XxD5n9QttpuIEZIfNDSYNzET5qvHCUuDYrQdKbK8kZxA692x80tQ
- Ironport-phdr: A9a23:PdGr+BVBwfwvOy7RXaf/k2tu3N7V8Kx9VTF92vMcY1JmTK2v8tzYMVDF4r011RmVB9ydsq4awLKH+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtViDanfL9/IxS7oQrNusQSnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRxj1hicaLD456H/YhdBsjKxVpxKhogZww4/SYIqIMPZzcafQcdYcSGFcXMheSjZBD5uyYYUPEeQPIOVWr4fyqFQSsBSxBxKhBP/zxjJSmnP6wbE23/onHArb3AIgBdUOsHHModvoLqgSVP2+wqzVzTXbcfxWwyr25Y/Tch87pPGMRah/ftHVyUkoFAPFk02QppL/Pz6OzuQNtHOb7/Z+WuKokWInrR9+oiS2y8oql4LGiZ4bxEre+iVl3IY6O8e4SEhjbNO4EpZeuSGXOopqTs4tQWxlpCg0x78HtJC0fyUHzJopyhHbZvGGfIaF4hLtWeafLDp5hX9oZryxiguu/Eauy+DxUNS/3lhNripAiNbMt3YN2gTJ6siGUfty4lmh1SyI1wDJ5eFIOVs0mrbbK54n3LEwl4QcsV7ZEiDqn0X2ibeadls+9uin9uvqZKjtqJyEN4Jslw3zMaQjlta+DOk6KAQDUWmW9f692bDj5UH0Q7FHgucrnqTWsZ3WP9oXqrClDwNPz4ou5QqzAjG729oCh3YHNkhKeBefgojpJV7OJPf4AO+6g1SrjTdr2+zKMqD7DpXVKXjDi6vhcqh660JG1QU808hT55NSCr4fPPL+QlL9ud/YAxMjMgG5wfzrBdt8248EWG+CAreVMKbIvl+J4uIvLfOMZIgQuDvlMPgq/fvujWcjllAGeamp2pgXaG2gHvt4OUWUemLsgtAaEWcWoAU+S/bmiFucXj5Pf3qyRb4z5iknCIK6CofOXpyigLuY3CuiApJWYn1GBUuXHHfzd4SEXu8MZziILs9glDwET7mhRJU72RGgrg+pg4Zge+HT42gTsY/p/Nlz/eza0x8ophJuCMHI6GiIB0Jphm4SD2st1aVnqEZ5zVSeyaViq+RfDsBe4LVPXxtsZs2U9PBzF92nAlGJRdyOUlvzHoTO6d4ZVtUq39IJJUBwB4f75vgm9zKtGKMYkPqNCYBmqso0PlD0INthky+AzK46k1QhBMdCZzXOuw==
On Sat, Jan 08, 2022 at 12:41:25PM -0600, Talia Ringer wrote:
> It's OK (inevitable I guess) to start with unverified hardware,
> though, and replace it later with hardware you verify (has anyone done
> that? It sounds cool).
Maybe not quite as you outlined. Still, possibly of interest:
https://riscv.org/blog/2020/05/getting-started-with-risc-v-verification/
Hardware is really hard to verify, though. Cf. dopant-level trojans,
etc:
https://www.schneier.com/blog/archives/2018/03/adding_backdoor.html
Sam
--
A: When it messes up the order in which people normally read text.
Q: When is top-posting a bad thing?
() ASCII ribbon campaign. Please avoid HTML emails & proprietary
/\ file formats. (Why? See e.g. https://v.gd/jrmGbS ). Thank you.
- [Coq-Club] A verified bootstrapping computer (academic curiousity), Talia Ringer, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Adam Chlipala, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Talia Ringer, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Andrei Popescu, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Marco Servetto, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Talia Ringer, 01/08/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Sam Kuper, 01/09/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Freek Wiedijk, 01/10/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Robert Solovay, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Jeremy Dawson, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Sam Kuper, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Freek Wiedijk, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Timothy Carstens, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), D. Ben Knoble, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Timothy Carstens, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Freek Wiedijk, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Sam Kuper, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Jeremy Dawson, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Robert Solovay, 01/11/2022
- Re: [Coq-Club] A verified bootstrapping computer (academic curiousity), Adam Chlipala, 01/08/2022
Archive powered by MHonArc 2.6.19+.