coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Formal Verification of a Safegcd Implementation in C for computing modular inverses
Chronological Thread
- From: "Russell O'Connor" <roconnor AT blockstream.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Formal Verification of a Safegcd Implementation in C for computing modular inverses
- Date: Tue, 14 Jan 2025 11:15:01 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=roconnor AT blockstream.com; spf=Pass smtp.mailfrom=roconnor AT blockstream.com; spf=None smtp.helo=postmaster AT mail-pj1-f41.google.com
- Ironport-data: A9a23:ozANfq3zqGwmtVWpO/bD5Vp1kn2cJEfYwER7XKvMYLTBsI5bpzAEy mtNCmGFbK3eNmH0eop0a9mx8h8C6pDXndNqSws53Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn8gVaYDkpOs/je8Eo24Kyo0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW1XQ8/5QDnw/AbwR9+JSMXwTy MVbeC9YO3hvh8ruqF66Yuxlh8BmNMuyeY1D4zdvyjbWCftgSpfGK0nIzYUAjXFg24YURKiYO 5NxhTlHNHwsZzVVPVwQDpQ5hs+ign70cCZEsl+coOw85G27IAlZiuC2aYKNJYbULSlTthiUl EX5r0anOyhEDcOz4mWq9luOpuCayEsXX6pJSeTgqa806LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDS9D8W1igoifBsEJFHdVXFOI+5UeGza+8Dxul6nYsYAJxY+IkicYKdDUn0 nq5go7UPH8/r+jAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj3nojqf4zQMaIYs3JJN3m/ 9ydQMEDa1g7iMcK0+Cj/wmCjW714JfOSQEx60PcWWfNAuJFiGyNNtDABbvztKkowGOlor+p4 iVsdy+2srxmMH11vHbRKNjh5Znwjxp/DBXSgER0A74q/Cm39niocOh4uW4lehg4aZ5VIma3O Cc/XD+9ArcDbBNGiocnM+qM5zgCl/CI+SnND6+EPoQROMAZmPGvo3w+OhT4M5/RfLgEyvxmY cjKL65A/F4VDqNoyDf+RuEWl9cWKtMWlAvuqWTA503/i9K2PSbLIZ9caQfmRr5jsMus/l6Om /4BbJvi9vmqeLeiCsUh2dROdQhSRZX6bLiqw/FqmhmreFM8Rz9+V6+JnNvMueVNxsxoqwsBx VnlMmcw9bY1rSSvxdyiOyE/OoD8F41yt2w6NiEKNFOlkSprK4W24atVM9N9cbA7/aYxhbR5X tsUSfWmW/5vczXg/yhCTJ/fqIc5Sg+nqzjTNAWYYR8+XaVaeSr3xvHecDDCzhI+VhiMiZNmo pmL9B/qfp4YdgEzUOfUcK2Oyn2yj1g8mcVzfUrCDYhRcR7KqINvFSz7taI1KZtUKDHo5DiT5 yCJCzg2+MjPpI4U9oHSpKam9o2GLcp3LnB4LUL6s4mkFHD90DK44IliVO2oQ2jsZFns8v//W dQPnuDODvIXuX1r7ax+Ku9P5oAj7YLNo7R68FxVLE/TZQ72NoI6c2i05ugRhKhj3bQDhBCXX HiI8dxkObmkHsPpPVoSBQg9ZNS4yvAmtWjO3MsxPXnFynd7zJifXWVWGiu8uihXAb92EYEim MMKmsod7S6hgRsLbPeCqA1p9Fq3E39RaJV/66kmA7LqhDE7lXBEQ5jXURHt7L+1Nt5jD0gNI x2vvpTkuYhy/ET4TicMJSD/5tYF3ZUqkzJW/WAGPGWMy4bkhOdo/Rh/8gYXbwVyzzdG2c0iO GEwERV+IJuO9Qw1hsIZB2GIMCNCDS2/5Ube5QYolmrYbk/wTU3LDjQ3Ftis9XAj0VB3X2Zk7 pDB70i9ShfsXsX6/hVqaH5fs/a5EOBArFzTqv6oD+GuPsccYwO8poSMeGBRiR/sIf1ptX39v eMwodpBM/zqBxUx/Z8+JZKRj4kLaRa+I2dHf/Ft0YUJEUzYexCwwTK+EF+wSOwcO8319VKEN OI2KvJtTxie0AO8ngIfD4MIIJ52m6cNz/gGcbXJO2UHkuW+qhxEjZHuzRX91VQbG4hWrcUAK 43qZ22jFE6UjiBqgGPjlpRPFVe5RtgmXzfC+t6J3t8HLL89ld19UFoT1+K0tkqFMQE88BOzu hjCVpDszOdj6NpNmtLsG5pcGw6bLsPXa9XQ1Tvutd4UPNXFHvrThllEtnjmIAVkEr8DUPtnl bm2kYDW3WGUmJ0UQmzmi526OK0R3vqLXc1TKdDSAEhBuymJSOvAwkIk1TijCJprlNh92JGWd zGgYpHtSe9PCsZv+nJFTgN/TTAfMv3TRYX9r3qfq/+sNEAs4TbfJon6yU6zPHBpTQ5WCZjQE QSuhu2P4Opfp4FyBBMpIfFqLpt7AV37U5sdaNzDmmiEP1asn2+9lOPupTg45RHPL0u0IsLwz JbGZxr5LTCZmqXDyvNHuI1T4DwTKltAgtcLQ0FMwO4u1giGD1MHI9pEYN9CQttRnzfp3Z71W CDVYSFwQW/hVDBDalPn7M6lQg6bAfcUN8zkIiAyuXmZcDqyGJjKFY4JGv2MOJuqUmCLICCbx dAiFrnYOxGwxtRxR79W6KDix+hgwfzeyzQD/kWVfwkexfoBKe1i6ZCjNFMlue/7/wXlnkHML msuWXpJSUT9Qkn0eSqlU2AAAwkX5VsD0B1xBRpiA7/jV0GzxulHw/7kJ/v+27hFZ8MPTFLLq bUbWEPVi12rNrcvVWfFdj7nbWKYyR5GIyRiEJLeeA==
- Ironport-hdrordr: A9a23:yMXK8qxtkpvQiquQvl3vKrPwAb1zdoMgy1knxilNoH1uA7Wlfq WV9sjzuiWE6gr5NEtQ+uxoW5PhfZq/z+8Q3WB5B97LNzUO01HYS72Kg7GSpQHIKmnR8qpz2a 98b7NzErTLfD1HpPe/zg39PdhI+ra6GWOT6ds2DU0BceinUc9dBs5CazqmLg==
- Ironport-phdr: A9a23:kGaviRPRJuFX5RpJLQsl6nZGBBdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDvqwr1QKXFtWAo9t/yMPo8InYGlY8qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebgtViDanfL9/L BS7oQrSu8QYnIBvNrs/xhzVr3RHfOhb2XlmKVWPkRji+8y+5oRj8yNeu/Ig885PT6D3dLkmQ LJbETorLXk76NXkuhffQwSP4GAcUngNnRpTHwfF9hD6UYzvvSb8q+FwxTOVPczyTbAzRDSi8 6JmQwLmhSsbKzI09nzch8pth6xZvR2hvQRyzIHUbo+bN/RwY73Tcs8BSGVbQspcTTZMDp+gY 4YNCecKIOZWr5P6p1sLtRayCxWiBP70yj9TmHD22ak62Pk4Hw3FwgEgGNQOsHLTrNXvOqsZT Oe4zLPPzTrfaPNW3zH96I/Sch06uv6MWbVwftbSyUk0CwPFlEufppbgPz+PyusNtG2b4vNmW OmyhGEptxt/rSKzxscwlIbJnIQVx0jL+yt3wos4K9+1RU1lbdOmEJZeuC+XOYV2T84gQmxlt zo3x7wItJKlfiUExpspygPfZfGEc4aG4gzuWeSPLTtkgn9uZbyxhxG38Ue6y+38UNG5301Or ipCjtbMtWsN1wDJ6seZUPR9+12t1iqI1wDW8u1ELkE0lbbbK5482bE8jIYcsUPGHiPumET2l LWadlkj+uSw8+TneLTmppmAOIBqlgH+NaIultahDuslLwgDWXWQ9+ek1LD740H1XLFHguc1n 6TZqpzWO9kXq6+jDwJaz4ou7Qu0Aimi0NQFhnkHMExKeAiagYjoOlDBPuj1Aeu5jl+xijlk3 erGMafkApjVLnjMjrPhfbFl5k5Z0gUzzNRf64tMCrEDPf7/Q0HxudPFAhMjPAy0xOHnCNp51 owAQ26AHqiZMKbKvV+J4OIgPfWMaZcLtDrhL/Up/f3jgH8jlVMDYKWk3IEbZX+lEvh+JkWWe 3vsgtMPEWcQuQo+SfTniEeFUTFPYHayWaQ85jYhCI+9FojDQoetj6CC3CegAp1WfH5JBUqJE Xvya4qEXPIMZDqUIsB6ijMET6SuS5c91RGysw/306drIvLO+iIErZLjyMR15+rLmB4u8jx0F t2R3H2JT2FphWwFXCQ23aB6oUxl0FiPy6l4g/pCFdxS/fxFSAk6NYSPh9B9Xtv1Q0fKesqDY FegWNSvRz8rHfwrxNpbKXxgAM6vihSL+GWBBLkTkKbBTMgu9anb2X72Pe53z3HN17I9lVQvR 41EMmjw1f03zBTaG4OcyxbRrK2tb6lJhEYllU+GxGuK5gRDVRJoFL/CVjYZb1fXqtLw4gXDS aWvAPIpKFgJ0taMf41NbNChllBaXLH7It2LeWW6nGG2AgygzLeLZ4nxZ38Q1SCbA08BwEgI5 XjTDQElHW+6pn7GSjlnFFbheUTppPN5o3S9SEgu5wuOaEZizKav9xcQw/ebTqBbxaoK7QEmr Tg8B1Ohx5TWBt6H8hJmZ7lZaMgh7U1v0GvYs0llPMXlIfw7wFEZdAtzsgXl0BAf5pxot88so TtqyQNzLfjdy1Zdb3aC2pu2PLTLK2709RTpaqjM21iY3szEsqEIoO81rVnupmTLXgIr7mln3 t9J0nCd+oSCDQwcVoj0W1o28B4yrq/TYy007YfZnXN2Nqz8vjjH0tMvTOwrr3ToN81YO6SCE gjoO8ceAMOtM/AwllGsKBkDOaEa9aI5Od+na+rTwLSib4MC1HqtiWVK5pw401rZrXItDL6Vm cxcnbfEh1jiNX+0llqqv8HplJoRYDgTGjD60i34HMtLYaY0e48XCGCoKsnxx9NkhperVWQLk TzrT14AxsKtfgKfKlLn2ggFn14Qqnuhnyyi5zZwlDoqtbaF0SXLhe/lcVBUXwwDDHknllrqL YWu2poAW0OvaQ4ujjOv4UHxxLNHvql2Ki/YRkICLE2UZylyF6C3sLSFectG7pgl5D5WXOqLa lefUrfhohEe3ksPBkNmzSsgP3Gvs5T9xVlhjX6FaWx0pzzfcN1xwhHW4JrdQ+RQ13wIXnswh T7SD1m6d96nmLfc343Euee4UWW7fpdXdiLo1p+auSK+o2ZtBFWzkuuyldvuDQUhmXWjhp86C GOS9Ui6PtCj3r/fU6ovZkRyAV7g98d2UppzlIc9ntBY2HQXgImU4WtSlG7yNdtB3qetJHEJR DMN35vU+F2/gBwlfi/PndunECnEka4DL5Ggb2gb2zww9ZVPAaaQtvlfmDdt50C/pkTXaOR8m TEUzb0v7mQbiqcHollIrG3VD7YMEE1fJSGpmQ6P6oX0tqJcY2CpdqKY3k55ltO6EKuPqwQaU 3H8MMRHf2c4/oBkPVTA3WemoJvjc97Wa9UJnheQlBzDlPRPJZs00PENgGA0XAC19W1gwOk9g xt02Ji8t4XSMGRh8pWyBRtAPyH0bcceqXn9yLxTlcGM08WzD41sT38VCYDwQ6viQ1dw/bz3c hyDGzompjKHFKrDSEWBvVx+oSuHEoj3ZSrKYiBIlZM4GEbbfAsF3EgVRGlowMJ/TFvxgpW/K AEhoWlAgzyw4hpUlrA2aV+mCj2Z/EHwLW1sAJmHcEgIsEcYuxaTYZTYtqUpR2lZ5sHz81bLc zDdPlUSSzlOAxzhZRirP6Hyt4actbHCW6zmaaOJOOvGqPQCBa7QldT2jdQgr3DUcZ/Wdnh6U 69ihREFBCElXZyfw3JWFUl132rMd5LJ/k/tvH0q6JnloLKzH1uwrYqXV+kIaIsppkDw2PbZc bbX3XcxKC4EhMlVmzmSk+lZhwRU02Y3JlzPWfwWvCrJBso8g4dxCBgWI2N2PcpMtecn2xVVf NTcgZXz36J5ifg8DxFEU0bgk4enf55CJWb1L17BCEuRUdbObTTW38H6Z7+9QrxMna1VsRO3o zOSD07kOHyKiTDoUxmlNewEgjucOVRSv4S0cxAlDmaGLpquchqgLNp+liE725Uxj3LOcHYea H1yLxoLobqX4idVxP54Hi0J73ZoK/WFhzfM7+TcLcVz07MjCSB1muRGpXUinuENvWcUGbovw XWU8oc9xjPu2vOCwTdmThdU/zNChYbR+F5nJb2c7J5LH3DN4BMK62yUTRUMvdpsTNP16MUyg pDCkrz+LDBa/pfa58wZUoLOL8mANnwmKzLjHDnfDxAZVzOiMCfUgEkXw5TwvjWF64M3rJThg s9EUrhASFk8De8XEGxgFd0GZY91B3Yqzefdg8kP6n6z6hLWQY8J2/KPHuLXCvLpJjGDiLBCb BZd2rL0I7MYMYjj0lBjYF139GwlM0DUWttOuTF7YwYx5k5K9SonJoXW80jhbQiu+2MJGPex2 BUxj1kmCQzM3DLl4lNyPliT4SVsyQ8+ntLqhT3Xezn0fv/YYA==
- Ironport-sdr: 67868d94_y6WfYSzXK12LY8O7SLyYnSgknuf7YEIiXevABJdvLzEMOcV LoKkxExW7l8tmHtCh6x0xmHXsY1sBkEbuNpc6jw==
Hi everyone.
We've recently completed our
project to formally verify libsecp256k1's implementation of (one of) its
modular inverse function.
For those interested, we have a blog post announcement that can be found at <https://blog.blockstream.com/formal-verification-of-the-safe gcd-implementation/>.
libsecp256k1 as an optimized C library for elliptic curve operations on the secp256k1 curve, a curve popularized by Bitcoin <https://github.com/bitcoin-core/secp256k1>. The modular inverse algorithm is an implementation of Bernstein and Yang's "Fast constant-time gcd and modular inversion" also known as "Safegcd" <https://gcd.cr.yp.to>. However, the particular variant we formalized is a variable-time one which is used during signature verification. We used the Verified Software Toolchain <https://vst.cs.princeton.edu/> to reason about the partial correctness of C functions.
The proof builds upon our previous work on verifying the correctness of the safegcd algorithm itself <https://blog.blockstream.com/a-formal-proof-of-safegcd-bounds>.
--
Russell O'Connor
- [Coq-Club] Formal Verification of a Safegcd Implementation in C for computing modular inverses, Russell O'Connor, 01/14/2025
Archive powered by MHonArc 2.6.19+.