coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Google Research summer Internship for building and formal verification of CHERIoT TCB (hardware and software)
Chronological Thread
- From: Murali Vijayaraghavan <vmurali AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Google Research summer Internship for building and formal verification of CHERIoT TCB (hardware and software)
- Date: Fri, 28 Feb 2025 11:20:10 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vmurali AT csail.mit.edu; spf=Pass smtp.mailfrom=vmurali AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing2021.csail.mit.edu
- Ironport-data: A9a23:GcFrIqjf6pWvuguuNtVWyLFrX1618hQKZh0ujC45NGQN5FlHY01je htvW2iFaPrba2Khe9EgPt7l9BsPuZfRmNJrQVRvpSw8FSpjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDtPg06/gEk35qmq4mlI5gdWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGLkozbI4j8fZNLz9y8 tgnEyEBYS6svrfjqF67YrEEasULK9T3M4QevH46lWuAS/09SJHHBaDL+ZlV0CpYasJmRKyOI ZFBL2ApM0Sojx5nYj/7DLogmfqyj33+WzZDoVOR4682/y7ewBEZPL3FaoONJIDRH54I9qqej m/39nvQWUlBDuPF6Aa+10iPisbq3gquDer+E5Xhq6cx2zV/3Fc7AxoPEFC/vPORkV+7Q9sZK koO+yNoo7JayaCwZt7gQxK/oXiL5EZGApxbCOQ77EeIy7aS7gqEboQZctJfQP4tsZ41fjc67 HHXo9TNOgd+vLKrZkvIo994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnE40L/Emd04OdJN3g/ w1muhTSkFn6sCLm/6Km4V/AgjSj/MCTF0g+/QzWWiSg7x8/aYK4D2BJ1bQ5xaseRGp6ZgDc1 JThpyR5xLpSZaxhbATXHI0w8EuVz/iEKibAplVkAoMs8T+gk1b6ItwIvmEnfR4xY5xdEdMMX KM1kV4KjHO0FCb3BZKbn6roUKzGMIC6Toq7Cq6IBjawSsIhLV7flM2RWaJg9zmwyRN3+U3OE ZKSat2lBnYHEql70CH+RuEGzb432zwzjWTdDYz2xBSh1r6Za2/9dFv2GAbmUwzN14vd+F+92 48GZ6O3J+B3CbyWSjPJ6rQaMV1iBSB9WPgaXeQOJ7bbemKL2QgJV5fs/F/WU9Y6xv0OxraTo ynVt40x4AOXuEAr4D6iMhhLAI4Dl74lxZ7iFX19bQSbyDI4bJyx7awSUZIycPN1vKZg1PN4B b1NMcmJHv0FGHyN9iU/fKvNitVoVC2qogaSYAujQjw0JKB7SyLzp9TLQwrI9Qs1NBSRi/cQm bOb+z3+fYsiXCVnVcbfV+KuxQi+vF8bg+NDYHHLKdhyJmTpodFmBCDvh8BqJeQOAATm/WaY3 Fy4GR0z+PXEk7Yowubz3IGFsIabPO9sFWVKH2TgzOiXNAuL2kGB0IN/QOKzUjSFb1zN+YKmf r9z3dznFf86wGZxrIt3Foh0wZIE59fAo6FQyiJmFi7pa2uHJ6xBIH7c++VyrYxIm6FkvDWpV nK1+tV1PauDPOXnGgUzICsnduGy6uEGqALN7PgaIFTI2wEvxeCpCX5tBhirjDBRCJBXM4l/m Ocoh5Mw2jyF0xEvNo6LszBQ+2GyNUc/aqQAtKwBIYrVmwEum0BjY5vdN3fM26uxSe5wa2skH jzFo5D5peV45lHDeH8NB3TyzbJjpZARiitrkn4GBXq0w+TguNFm/Sd/0zoNSiZt8i5myMN2Y 2hiCF10L/6B/hBun8lyYFqvEABgWjyc3F7A9F8SsGiAV0WDC2j/DFA8Hc2v/0kp1X1WURYG3 bOfyUfjCS3LeuOo1AQMeEdVkd7RZv0vyR/zw+WcANWjI5k2RRHHk52eTzMEhDW/CPxgmXCdg /dh+dhBTJHSNAkSkvUdMJab37FBcyK0DjVObt859ZxYAFyGXi+53AWPDEWDesltAfju2m3gA uxMIvN/bTiP5BysnBs6W5FVe6RVmcQ37uUsYrnofG4Kk4WOpwpT7a7/yHLMu38Jcf5Pz+AGN YLjRxCTGDexhFxVuVP3gutqB26aWeQANSrAhL2b0eNRDJ8SkvBeQWdr2JuOgnilGg9G/RWVg QD9W5Hr39FSkbpLoY+9PZhAViOVKMzyXtum6AqckcpDRvKRPNbstzE6kEjGPQNXDOA3W91Ii qmHj9qv+Eb7v7oNcnv4nqOZHPJj/vSCX+twM+P2IkJFnCCEZtTe3hsb9028Kr1LiNl75MK3Y yeZMeyeLcU0XfVZz11rMxluKQ4XUfnLX/2xtBGDoOSpITlD9w7+dfeM12LjNENffQ82Y6zOM Bf+4auS14oJvbZ3JUE2At99CMVFO37lY6wtcuPxuRS+DmWFhlCjuKPopSE/6APkW2W1L8Ln3 a3rHhTOVgy+mKXt/uFrt4Zfuh42DnEkpcISekkb2cB9ihHkLWogANkeD647CcBvonSv7K37W TDDUjJzQ2G1FzFJag7179nfTx+STL5GcMvwIjsyuViYcWGqDYeHG6Fs7Tpk/2wwQDb40eW7M psLzxUc5PRqLk1BHo7/J8BXgNuLAtvd224H/kH7nJaqWU9YCq4D1XgnGQtREyHLDqkhUakNy XcdHQh5rIOTECYd0vqMv1ZeAxgYuHXqziluYCuSqDoak5vO1/VOkZUTJMmquoDur602yHomT mj+Rm/L5mGKnHEfpMPFfj7vbbBcUZq2IyRxEEMvqcD+UU19BqTL8v7uRRYycfw=
- Ironport-hdrordr: A9a23:jC4sEasiea11BmqDzF44TLyG7skDv9V00zEX/kB9WHVpm62j5r uTdZEgviMc5wxhPU3I9erwWpVoBEmslqKdgrNxAV7BZniBhILAFugLh+bfKn/bexEWndQtrJ uIHZIOcOHYPBxViYLU7AGkD80t2rC8gceVbCTlo0tFfEVFb6lh6kNeEQaUEkp/QU1jCYAiHJ SRouprzgDQHUj/ov7VOpDNZYb+m+E=
- Ironport-phdr: A9a23:dkZJ1x/FeO2+4P9uWe+2ngc9DxPPW53KNwIYoqAql6hJOvz6uci5Z gqHvb493QSYFazgqNt6yMPu8JrcEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/9pPNbwlSmDaxfbx+I RayoAjfssQdnJdvJLs2xhbVrXREfPhby3lvKVyPgRj3+92+/IRk8yReuvIh89BPXKDndKkmT rJWESorPXkt6MLkqRfMQw2P5mABUmoNiRpHHxLF7BDhUZjvtCbxq/dw1zObPc3ySrA0RCii4 qJ2QxLmlCsLKzg0+3zRh8dtjqxUvQihqgRwzI7aYo6bNPRwcKDAc90EWWVMRdxeWzBbD46mc 4cDE+gMMOBFpIf9vVsOqh6+CBGrCuPy0D9HnHv23awn2OsuEAHG3hYvHtIUv3TOttr1O6cSX vqrzKbSyzXIcvRb2Sn46IjVaBAuu/WMXbNrfMXN0kkgDQLFjlGKpYzgPjOVyv4BvHaG4Op9T O+ijXMspA5trDa13MgslpXJiZwPylDC7Sh13oI4K9KmRUNnf9KpEp9dujyHOoZ0Qs0uX39lt To6xLMIuZO2YigHxYg5yxPBa/GJfImF7BL/WOqMITl1i2xpdbSijBi89kigz/fzVsiy0FtSs iVFksfDtmoM1xzU9siLUPx9/l2u2TqX2ADT6/1EIUAplaXAMZIu3rkwlp8LvUTGHy/2hF/6g 7GLeUU54uSo5OPnYrLppp+YKYB4kB3xMqMrmsG5HO82MRAOUnCG9eii17Dv50P0TKlQgvEoi KXUspPXKdwFqqKlBwJZyIUu5halAzu4zdgVnmMLIV1LdR+BkoPkJVXOIO3jDfejnVusiiplx /HHP7L/GpjBMn7Om6r7c7ln8U5T0g8zwMhf551KDrEBJ+r+WkjstNzEAR85NA20w+DoCNljy o8SR3+DDrWFP6PJq1CI5+YvL/OJZI8UpDbxMeYq6OPzjXMhmF8de7em3YcPZXylAPhrIF+Vb HTwjtsbD2sGpAgzQe/yhF2HSzFTZnKyX6wm5jE8DYKrFZnDRoWwgLybxii7GpxWa3taBVCXC 3jodoGEV+0JaCKTPs9tiCILWqW8S4M50xGhrxf1y6B7IerM5i0YqZXj2cBo6+HLjxE96SR0D 9iB02GKV2x7gmQIRyYv0K9jpUx910yM3LNjg/1YENxT/+lGXh07NZ7a1ex6Csr9VhjPfteTG x6aRYCtBih0RdYsyfcPZVx8EpOslEPtxS2vVpoIjbWPBdQK86DVznHrLsl9wmjP0uF1kVw7W MJLNEWtnad+807WBpKPnkmEwfX5PZ8A1TLAoT/QhVGFu1tVBVYYucTtWHkeYhGTttHl/gbYS LToD707MwxHwMrEK61Qa9Svg08VDOz7NoH4ZGS803y1GQ7O3qmFOZTvZn8U2CT1A1MNkgRV+ HeacwUyG3TpuHrQWQRnDkmneEbw6a97oXK/QFUzylSUalB73r600hUOjP2YDfYSwvQJtDpy4 y5sEgOb2NTbQ8GFuxInfKhYZoYl50xb0GvCqwFnFpu9M69lh1gRKVwt5gXlzBx2DsNFkNRso X83pOZrAYSf1l4JNzaR3JSqf6bSNnG35hekLajfxlDZ1t+SvKYJ8vUx7Vv57kmvEQI5/nNr3 sMwsTPU74jWDAcUTZP6U1omvxl8qbbAZyAh5oTSnXRyOKiwuzXG1ponHuwgghqnet5eNuuDG mqQW4UEAtW0Iegrs1OyZxMAeuVT6Og5M97nP/qK1ai3PfpxySq8hDcP64R830SQsitkH7eSj 9Bem7fCmFTXBFKexB+7v8v6mJ5Jf2QXF2u7k23/AZJJI7d1dsANAHuvJMu+wpN/gYTsUjhW7 g3GZRtO1cm3dB6Vd1G40xdX0BFdv3m6gyK8zhR/iDgoquya3TCIzuj/PkliWCYDVCx5gFHgL JLhxc4fQVKhawkBnwCs5EK8wqlH4qlzMiOAJCUANzizJGZkXKyqs7OEaMMa85IkvxJcV+Gka EybQLrwy/cD+xvqBHAWhDUydjXw/478gwQ/kmWWanB6sHvef8h0gxbZ/t3VA/BLjHIKQyxxi D+fAVbZXZHh49CJjZ7Hs8i1TGugUttWcDWtwI+d/Ce2/mxlBxSjkuv7w4e3V1Nil3W9iIkiX D6AtBvmZ4j3y6m2VIAvNlJlAlPx8YsyG41zlJcxmIBF3HEbgpuP+n9U2Wz3MNhdxef/dC9UH 25NmIaTuk66iB4GTDrB3Y/yW3SDz9E0YtC7ZjlTwSch94VQD6zS6rVYnCxzq17+rATLYPE7k C1OrJlmoHMcnewNvxIgiyuHBbVHV1ddIDblkxWg5Mu3raERYWezN7W8yQAt+LLpRKHHuQxaV HvjL908GDJq58F+GFnX2Xz3rITlZJ/dYc9Z5Xj221/QyuNSLpw2jP8DgyFqbHn8sXMSwOk+l RVy3Ju+sdvPOyB38am+GBIdKiztapZZ5GT2lagH1JXzvcjnDtB7Fz4MRpetUf+4DGdYq6H8L wjXWDwk9iXCQ+qZRlfZsAE+6CuSW5GzayPOdD9Dk5M6AkHafRI64khcXS1mzMdpUFvzgpSnK AAguHgQ/gKq80EcjL8ycUG5CiCG+k+pcmlmEsbHd0gKtllLtRWSapbW9v5pVyRIm//p5A2LI WiGawkaCGAVHEGIGhj1N72qr7Es6sC+AeyzZ7vLaLSK86lFUuuQgIio2c1g9iqNMcOGOj9jC ec60wxNRyIxHcORgDgJRyEN8kCFJ8eGuBex/DF2pcGj4bzqXgzo/46GF7pVN51m5Rm3ha6JM +PYijx+LH5U0ZYFxHmAz7Z6vhZakyZ1azykCqgNrwbKUb7fna5RAERDMXo1P9BB7qZ62whRf 8PXl5K917J1iOI0F0YQVVHlnZLMB4RCKGW8OVXbQUeTYe3cdXuQm4etJ/zsGtgyxK1Ouha9u CiWCRrmNzWHzXzyUgy3dPtLh2edNQBfv4e0dlBsD3LiRZTocE7eUpc/gDsozLkznn6PO3QbN G02bUZQtLSU7AtTmfx+HypE72YjIOWZ0XX8jaGQOtMNvP1nDz4h3fpd+2g/wqBJ4TtsQ+Fpl yzTqNE0+wv/1OKUwztjFh9PtnBGiJ/B7iAAce3Js5JHX3jD5hcE626dXg8Lq9VSAdrqo6lMy 9LLmcobyR9F7s7b+soaCJKMcpvBO2EoMB6vHT/ISgYJUGzzXYkwr0dGmfCWsHiUst43poW+w fLmr5dQT1U0ErUfC1gjEdAfcs8fYw==
- Ironport-sdr: 67c20c7a_k4r2Pa2Zv0FlEf258AM0TFpnIs0lfqpHq6+UV9BtCt1FfNF 93Y7AIzJpJ6p87p8lXYcpL3tUWDGjnsk5Ut4Lhg==
Hi all
Note that, unfortunately, the deadline is literally today (Feb 28 2025 PST = UTC-8). My apologies for posting it so late - there were some logistics issues that had to be sorted out.
Thanks
Murali
We have a Google Research summer internship position open for an ambitious project involving
a) building a CHERIoT hardware system (in a Coq DSL called Kami based on earlier research work), including adding RISC-V vector extensions to CHERIoT,
b) formally verifying the functional correctness of the hardware system with respect to an ISA spec (written in Kami itself, and if being more ambitious, prove it against the Sail specs also),
c) formally verifying the security properties of the low-level compartment/thread switcher TCB, including proving that fully isolated compartments behave as if they run on air gapped machines.
The idea is to work with the Google Research team (in Mountain View) to do a subset of these efforts during the summer internship and collaborate further in the future. While working in Mountain View is preferred, we are open to hybrid/remote (within US) positions. If interested, please apply to Research Internship:
a) building a CHERIoT hardware system (in a Coq DSL called Kami based on earlier research work), including adding RISC-V vector extensions to CHERIoT,
b) formally verifying the functional correctness of the hardware system with respect to an ISA spec (written in Kami itself, and if being more ambitious, prove it against the Sail specs also),
c) formally verifying the security properties of the low-level compartment/thread switcher TCB, including proving that fully isolated compartments behave as if they run on air gapped machines.
The idea is to work with the Google Research team (in Mountain View) to do a subset of these efforts during the summer internship and collaborate further in the future. While working in Mountain View is preferred, we are open to hybrid/remote (within US) positions. If interested, please apply to Research Internship:
Note that, unfortunately, the deadline is literally today (Feb 28 2025 PST = UTC-8). My apologies for posting it so late - there were some logistics issues that had to be sorted out.
Thanks
Murali
- [Coq-Club] Google Research summer Internship for building and formal verification of CHERIoT TCB (hardware and software), Murali Vijayaraghavan, 02/28/2025
Archive powered by MHonArc 2.6.19+.