{"id":324553,"date":"2021-06-08T15:00:09","date_gmt":"2021-06-08T15:00:09","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=324553"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=324553","title":{"rendered":"\u041a\u0430\u043a \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c Python \u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 Signal"},"content":{"rendered":"\n<div class=\"post__text post__text_v2\" id=\"post-content-body\">\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/c1e\/0d4\/6ef\/c1e0d46efd88b2e67f4e45c311d0d013.jpg\" width=\"780\" height=\"440\"><figcaption><\/figcaption><\/figure>\n<p>Galois \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u043d\u0430\u0434 \u043f\u043e\u0432\u044b\u0448\u0435\u043d\u0438\u0435\u043c \u0443\u0434\u043e\u0431\u0441\u0442\u0432\u0430 <a href=\"https:\/\/saw.galois.com\/\">SAW<\/a>, \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u0430 \u0434\u043b\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043d\u0430&nbsp;C&nbsp;\u0438&nbsp;Java, \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u043a\u043e\u0434 \u043a\u0442\u043e\u0440\u043e\u0433\u043e \u043e\u0442\u043a\u0440\u044b\u0442. \u041e\u0441\u043d\u043e\u0432\u043d\u044b\u043c \u0441\u043f\u043e\u0441\u043e\u0431\u043e\u043c \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0435\u0439 \u0441&nbsp;SAW \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0435\u0433\u043e \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438&nbsp;\u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u0446\u0435\u043d\u0430\u0440\u0438\u0435\u0432. \u0427\u0442\u043e\u0431\u044b \u0441\u0434\u0435\u043b\u0430\u0442\u044c SAW \u043a\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u0431\u043e\u043b\u0435\u0435 \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u043c, \u0432&nbsp;\u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u044f\u0437\u044b\u043a\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f SAW \u0442\u0435\u043f\u0435\u0440\u044c \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c Python! \u0414\u043b\u044f \u0434\u0435\u043c\u043e\u043d\u0441\u0442\u0440\u0430\u0446\u0438\u0438 \u044d\u0442\u043e\u0439 \u043d\u043e\u0432\u043e\u0439 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0432 Galois&nbsp;\u0441\u043e\u0437\u0434\u0430\u043b\u0438 \u043f\u0440\u0438\u043c\u0435\u0440, \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u0432 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0443 \u0447\u0430\u0441\u0442\u0438 <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\">\u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438<\/a> \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 Signal \u043d\u0430&nbsp;\u044f\u0437\u044b\u043a\u0435&nbsp;\u0421.&nbsp;\u0412 \u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, \u043a\u0430\u043a \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f SAW \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0442\u0441\u044f \u0443\u0441\u043b\u043e\u0432\u0438\u044f, \u043f\u0440\u0438 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 Signal \u0431\u0443\u0434\u0435\u0442 \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u0430\u0443\u0442\u0435\u043d\u0442\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043e. \u041a \u0441\u0442\u0430\u0440\u0442\u0443 \u043a\u0443\u0440\u0441\u0430 \u043e <a href=\"https:\/\/skillfactory.ru\/python-for-web-developers?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_PWS&amp;utm_term=regular&amp;utm_content=080621\">Fullstack-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0435<\/a> \u043d\u0430 Python \u043c\u044b \u043f\u0435\u0440\u0435\u0432\u0435\u043b\u0438 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u043e\u0431 \u044d\u0442\u043e\u043c \u043f\u0440\u0438\u043c\u0435\u0440\u0435.<\/p>\n<hr>\n<h3>SAW-\u043a\u043b\u0438\u0435\u043d\u0442 Python<\/h3>\n<p>\u0423\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 SAW \u043c\u043e\u0436\u0435\u0442 \u043e\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043b\u044f\u0442\u044c\u0441\u044f \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u0430\u043c\u0438 Python \u0447\u0435\u0440\u0435\u0437 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0443 saw-client \u0432&nbsp;<a href=\"https:\/\/pypi.org\/\">PyPI<\/a>. \u0420\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e Python \u043d\u0435&nbsp;\u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438&nbsp;\u2014 \u0443\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 SAW \u043e\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0447\u0435\u0440\u0435\u0437 JSON-RPC API, \u043a\u0430\u043a \u043f\u043e\u043a\u0430\u0437\u0430\u043d\u043e \u0432&nbsp;<a href=\"https:\/\/galois.com\/blog\/2020\/10\/demo-control-saw-from-any-language\/\">\u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0441\u0442\u0430\u0442\u044c\u0435<\/a>. \u0411\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 saw-client \u043f\u043e\u0441\u0442\u043e\u044f\u043d\u043d\u043e \u0440\u0430\u0437\u0432\u0438\u0432\u0430\u043b\u0430\u0441\u044c, \u0438&nbsp;\u0442\u0435\u043f\u0435\u0440\u044c \u0432&nbsp;\u043d\u0435\u0439 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d \u0432\u044b\u0441\u043e\u043a\u043e\u0443\u0440\u043e\u0432\u043d\u0435\u0432\u044b\u0439 \u0438\u043d\u0442\u0435\u0440\u0444\u0435\u0439\u0441, \u043e\u0442\u0432\u0435\u0447\u0430\u044e\u0449\u0438\u0439 \u0437\u0430&nbsp;\u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u0439 RPC.<\/p>\n<p>\u041f\u043e\u043c\u0438\u043c\u043e Python, \u0432&nbsp;SAW \u0442\u0430\u043a\u0436\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0430\u043b\u044c\u0442\u0435\u0440\u043d\u0430\u0442\u0438\u0432\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u0446\u0435\u043d\u0430\u0440\u0438\u0435\u0432, \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u044b\u0439 SAWScript. \u0425\u043e\u0442\u044f \u043d\u0430&nbsp;SAWScript \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e \u043f\u0438\u0441\u0430\u0442\u044c \u0442\u0435&nbsp;\u0436\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438, \u0447\u0442\u043e \u0438&nbsp;Python, \u044d\u0442\u043e\u0442&nbsp;\u044f\u0437\u044b\u043a&nbsp;\u043d\u0435&nbsp;\u043b\u0438\u0448\u0451\u043d \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043a\u043e\u0432. SAWScript&nbsp;\u2014 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u044f\u0437\u044b\u043a, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043e\u043d&nbsp;\u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u0441\u043b\u043e\u0436\u0435\u043d \u0434\u043b\u044f \u043f\u043e\u043d\u0438\u043c\u0430\u043d\u0438\u044f \u0442\u0435\u043c\u0438, \u043a\u0442\u043e \u0432\u043f\u0435\u0440\u0432\u044b\u0435 \u0431\u0435\u0440\u0451\u0442\u0441\u044f \u0437\u0430&nbsp;\u0438\u0437\u0443\u0447\u0435\u043d\u0438\u0435&nbsp;SAW. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0432&nbsp;SAWScript \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043f\u043e\u0434\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u044f \u0432\u043d\u0435\u0448\u043d\u0438\u0445 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a. \u0415\u0441\u043b\u0438 \u0432\u044b&nbsp;\u0437\u0430\u0445\u043e\u0442\u0438\u0442\u0435 \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043d\u0430&nbsp;SAWScript \u0442\u043e, \u0447\u0435\u0433\u043e \u043d\u0435\u0442 \u0432&nbsp;\u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u043e\u0439 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435, \u0432\u0430\u043c \u043f\u0440\u0438\u0434\u0451\u0442\u0441\u044f \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u043d\u0443\u0436\u043d\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u0441\u0430\u043c\u043e\u0441\u0442\u043e\u044f\u0442\u0435\u043b\u044c\u043d\u043e.<\/p>\n<p>\u0421&nbsp;\u0434\u0440\u0443\u0433\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, Python&nbsp;\u2014 \u0448\u0438\u0440\u043e\u043a\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u044f\u0437\u044b\u043a, \u0438\u0437\u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e \u0445\u043e\u0440\u043e\u0448\u043e \u0437\u043d\u0430\u043a\u043e\u043c\u044b\u0439 \u0433\u043e\u0440\u0430\u0437\u0434\u043e \u0431\u043e\u043b\u044c\u0448\u0435\u043c\u0443 \u0447\u0438\u0441\u043b\u0443 \u043b\u044e\u0434\u0435\u0439. \u0423&nbsp;Python \u0442\u0430\u043a\u0436\u0435 \u0438\u043c\u0435\u0435\u0442\u0441\u044f \u0431\u043e\u0433\u0430\u0442\u044b\u0439 \u043d\u0430\u0431\u043e\u0440 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a \u0438&nbsp;\u0432\u0441\u043f\u043e\u043c\u043e\u0433\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c, \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u0445 \u0432&nbsp;\u043a\u0430\u0442\u0430\u043b\u043e\u0433\u0435 PyPI. \u0414\u0430\u0436\u0435 \u0435\u0441\u043b\u0438 Python \u043d\u0435&nbsp;\u0432\u0445\u043e\u0434\u0438\u0442 \u0432&nbsp;\u0447\u0438\u0441\u043b\u043e \u0432\u0430\u0448\u0438\u0445 \u043b\u044e\u0431\u0438\u043c\u044b\u0445 \u044f\u0437\u044b\u043a\u043e\u0432 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u043c\u044b&nbsp;\u0432\u0441\u0451 \u0440\u0430\u0432\u043d\u043e \u0441\u043e\u0432\u0435\u0442\u0443\u0435\u043c \u043f\u043e\u043f\u0440\u043e\u0431\u043e\u0432\u0430\u0442\u044c saw-client. \u0415\u0441\u043b\u0438 \u043f\u043e\u0434 \u0440\u0443\u043a\u043e\u0439 \u043d\u0435&nbsp;\u043e\u043a\u0430\u0436\u0435\u0442\u0441\u044f \u043d\u0438\u0447\u0435\u0433\u043e \u0434\u0440\u0443\u0433\u043e\u0433\u043e, \u043a\u043e\u0434, \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u044b\u0439 \u0432&nbsp;saw-client, \u043c\u043e\u0436\u0435\u0442 \u043f\u043e\u0441\u043b\u0443\u0436\u0438\u0442\u044c \u0438\u0441\u0442\u043e\u0447\u043d\u0438\u043a\u043e\u043c \u0432\u0434\u043e\u0445\u043d\u043e\u0432\u0435\u043d\u0438\u044f \u0434\u043b\u044f \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u0430\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u043e\u0433\u043e \u043a\u043b\u0438\u0435\u043d\u0442\u0430 \u043d\u0430&nbsp;\u0434\u0440\u0443\u0433\u043e\u043c \u044f\u0437\u044b\u043a\u0435.<\/p>\n<h3>\u0411\u0430\u0437\u043e\u0432\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0432&nbsp;saw-client<\/h3>\n<p>\u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c, \u043a\u0430\u043a saw-client \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0439 \u0440\u0435\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u043d\u0430&nbsp;\u044f\u0437\u044b\u043a\u0435&nbsp;C. \u0414\u043b\u044f \u043f\u0440\u0438\u043c\u0435\u0440\u0430 \u0432\u043e\u0437\u044c\u043c\u0451\u043c <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\">libsignal-protocol-c<\/a>. \u042d\u0442\u0430 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u043d\u0430&nbsp;\u044f\u0437\u044b\u043a\u0435 C&nbsp;<a href=\"https:\/\/en.wikipedia.org\/wiki\/Signal_Protocol\">\u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b Signal<\/a>, \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u0434\u043b\u044f \u0448\u0438\u0444\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u043c\u0433\u043d\u043e\u0432\u0435\u043d\u043d\u044b\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u0433\u043e\u043b\u043e\u0441\u043e\u0432\u044b\u0445 \u0438&nbsp;\u0432\u0438\u0434\u0435\u043e\u0437\u0432\u043e\u043d\u043a\u043e\u0432. \u042d\u0442\u043e\u0442 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u0442\u0441\u044f \u0432&nbsp;<a href=\"https:\/\/signal.org\/\">\u043f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u0438 Signal Messenger<\/a>, \u043f\u043e\u043b\u0443\u0447\u0438\u0432\u0448\u0435\u043c \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u0435 \u043f\u043e&nbsp;\u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0443, \u043d\u043e&nbsp;\u0442\u0430\u043a\u0436\u0435 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u0432&nbsp;\u0434\u0440\u0443\u0433\u0438\u0445 \u043f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u044f\u0445, \u0442\u0430\u043a\u0438\u0445 \u043a\u0430\u043a WhatsApp, Facebook Messenger \u0438&nbsp;Skype.<\/p>\n<blockquote>\n<p>\u041e\u0431\u0449\u0435\u0435 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u0435\u0439 SAW \u0441&nbsp;\u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 libsignal-protocol-c \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u043d\u043e \u0432&nbsp;\u0440\u0430\u0437\u0434\u0435\u043b\u0435 &#171;\u041f\u043b\u0430\u043d\u044b&#187;.<\/p>\n<\/blockquote>\n<p>\u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0431\u0430\u0437\u043e\u0432\u0443\u044e \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0443 \u0434\u0430\u043d\u043d\u044b\u0445, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u0443\u044e \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u043e\u0439 libsignal-protocol-c, \u0430&nbsp;\u0438\u043c\u0435\u043d\u043d\u043e <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\/blob\/3a83a4f4ed2302ff6e68ab569c88793b50c22d28\/src\/signal_protocol_internal.h%23L18-L21\">signal_buffer<\/a>:<\/p>\n<pre><code class=\"cpp\">struct signal_buffer {     size_t len;     uint8_t data[]; };<\/code><\/pre>\n<p>signal_buffer \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0439 \u043c\u0430\u0441\u0441\u0438\u0432 (\u043c\u0430\u0441\u0441\u0438\u0432 \u0434\u0430\u043d\u043d\u044b\u0445) \u0441&nbsp;\u0434\u043b\u0438\u043d\u043e\u0439&nbsp;len. \u041f\u0440\u0438 \u043e\u0442\u043f\u0440\u0430\u0432\u043a\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e libsignal-protocol-c \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u043c \u043a\u043e\u043c\u043f\u043e\u043d\u0435\u043d\u0442\u043e\u043c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f signal_buffer.<\/p>\n<p>\u0427\u0442\u043e\u0431\u044b \u0431\u044b\u0442\u044c \u0443\u0432\u0435\u0440\u0435\u043d\u043d\u044b\u043c, \u0447\u0442\u043e libsignal-protocol-c \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0442\u0430\u043a, \u043a\u0430\u043a \u0437\u0430\u044f\u0432\u043b\u0435\u043d\u043e, \u043d\u0443\u0436\u043d\u043e \u0443\u0431\u0435\u0434\u0438\u0442\u044c\u0441\u044f, \u0447\u0442\u043e \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 signal_buffer \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u043e\u0436\u0438\u0434\u0430\u0435\u043c\u043e\u043c\u0443. \u0411\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0435 \u0434\u0432\u0443\u0445 \u0431\u0443\u0444\u0435\u0440\u043e\u0432 signal_buffer \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\/blob\/3a83a4f4ed2302ff6e68ab569c88793b50c22d28\/src\/signal_protocol.c%23L591-L603\">signal_constant_memcmp<\/a>:<\/p>\n<pre><code class=\"cpp\">int signal_constant_memcmp(const void *s1, const void *s2, size_t n) {     size_t i;     const unsigned char *c1 = (const unsigned char *) s1;     const unsigned char *c2 = (const unsigned char *) s2;     unsigned char result = 0;      for (i = 0; i &lt; n; i++) {         result |= c1[i] ^ c2[i];     }      return result; }<\/code><\/pre>\n<p>\u0418\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e \u043f\u043e\u043d\u044f\u0442\u043d\u043e, \u0447\u0442\u043e \u0443\u0442\u0438\u043b\u0438\u0442\u0430 signal_constant_memcmp \u0434\u043e\u043b\u0436\u043d\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c, \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u043e&nbsp;\u043b\u0438 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u0434\u0432\u0443\u0445 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432 signal_buffer. \u0415\u0441\u043b\u0438 \u043e\u043d\u0438 \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b, \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0432\u0435\u0440\u043d\u0451\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435&nbsp;0. \u0415\u0441\u043b\u0438 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u043d\u0435&nbsp;\u0441\u043e\u0432\u043f\u0430\u0434\u0430\u0435\u0442, \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442\u0441\u044f \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u0443\u043a\u0430\u0437\u044b\u0432\u0430\u044e\u0449\u0435\u0435 \u043d\u0430&nbsp;\u0431\u0430\u0439\u0442\u044b, \u0432&nbsp;\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u044b \u043e\u0442\u043b\u0438\u0447\u0430\u044e\u0442\u0441\u044f.<\/p>\n<p>\u041f\u0440\u0438 \u044d\u0442\u043e\u043c \u043d\u0430&nbsp;\u043f\u0435\u0440\u0432\u044b\u0439 \u0432\u0437\u0433\u043b\u044f\u0434 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043d\u0435\u043e\u0447\u0435\u0432\u0438\u0434\u043d\u043e, \u0447\u0442\u043e \u043f\u0440\u0438 \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u0430\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0432\u0435\u0440\u043d\u0451\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435&nbsp;0. \u0423\u0447\u0438\u0442\u044b\u0432\u0430\u044f, \u0447\u0442\u043e \u043c\u0430\u043d\u0438\u043f\u0443\u043b\u044f\u0446\u0438\u0439 \u0441&nbsp;\u0431\u0438\u0442\u0430\u043c\u0438 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043c\u043d\u043e\u0433\u043e, \u0432\u043f\u043e\u043b\u043d\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e, \u0447\u0442\u043e \u043a\u0442\u043e-\u0442\u043e \u043c\u043e\u0433 \u0434\u043e\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u043e\u0448\u0438\u0431\u043a\u0443 \u043f\u0440\u0438 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0438\u0438 \u043a\u043e\u0434\u0430, \u043c\u0430\u043d\u0438\u043f\u0443\u043b\u0438\u0440\u0443\u044e\u0449\u0435\u0433\u043e \u0431\u0438\u0442\u0430\u043c\u0438. \u041f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0442\u0430\u043a\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c, \u0441\u0432\u0435\u0440\u0438\u0432 \u0435\u0433\u043e \u0441\u043e&nbsp;\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0435\u0439, \u0441\u043e\u0437\u0434\u0430\u043d\u043d\u043e\u0439 \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e saw-client. \u0422\u0430\u043a\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043c\u043e\u0436\u0435\u0442 \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u0442\u044c \u043f\u0440\u0438\u043c\u0435\u0440\u043d\u043e \u0442\u0430\u043a:<\/p>\n<pre><code class=\"python\">from saw_client.llvm import *  class ConstantMemcmpEqualSpec(Contract):     def specification(self) -&gt; None:         _1          self.execute_func(_2)          _3<\/code><\/pre>\n<p>\u041a\u043b\u0430\u0441\u0441 Contract \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u0442 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 SAW \u0441&nbsp;\u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u043c\u0435\u0442\u043e\u0434\u0430 specification. \u0427\u0442\u043e\u0431\u044b \u0441\u043e\u0437\u0434\u0430\u0442\u044c \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u0443\u044e \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e, \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0441\u043e\u0437\u0434\u0430\u0442\u044c \u043f\u043e\u0434\u043a\u043b\u0430\u0441\u0441 Contract \u0438&nbsp;\u043f\u0435\u0440\u0435\u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u043c\u0435\u0442\u043e\u0434 specification. \u041a\u0430\u0436\u0434\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0441\u043e\u0441\u0442\u043e\u0438\u0442 \u0438\u0437&nbsp;\u0442\u0440\u0451\u0445 \u0447\u0430\u0441\u0442\u0435\u0439:<\/p>\n<ul>\n<li>\n<p>\u041f\u0440\u0435\u0434\u0432\u0430\u0440\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u044f (_1), \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0449\u0438\u0435 \u0434\u043e\u043f\u0443\u0449\u0435\u043d\u0438\u044f, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u043f\u0435\u0440\u0435\u0434 \u0432\u044b\u0437\u043e\u0432\u043e\u043c \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438.<\/p>\n<\/li>\n<li>\n<p>\u0410\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u044b \u0434\u043b\u044f \u043f\u0435\u0440\u0435\u0434\u0430\u0447\u0438 \u0432&nbsp;\u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e (_2).<\/p>\n<\/li>\n<li>\n<p>\u041f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u044f (_3), \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0449\u0438\u0435 \u0445\u0430\u0440\u0430\u043a\u0442\u0435\u0440 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043f\u043e\u0441\u043b\u0435 \u0432\u044b\u0437\u043e\u0432\u0430 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438.<\/p>\n<\/li>\n<\/ul>\n<p>\u0423\u0447\u0438\u0442\u044b\u0432\u0430\u044f \u0442\u0440\u0435\u0431\u043e\u0432\u0430\u043d\u0438\u044f \u043a&nbsp;\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u043c, \u043a\u0430\u043a \u0443\u0442\u0438\u043b\u0438\u0442\u0430 signal_constant_memcmp \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0432 \u043f\u0440\u0435\u0434\u0435\u043b\u0430\u0445 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 SAW:<\/p>\n<pre><code class=\"python\">class ConstantMemcmpEqualSpec(Contract):     n: int      def __init__(self, n: int):         super().__init__()         self.n = n      def specification(self) -&gt; None:         s1  = self.fresh_var(array_ty(self.n, i8), \"s1\")         s1p = self.alloc(array_ty(self.n, i8), points_to = s1)         s2  = self.fresh_var(array_ty(self.n, i8), \"s2\")         s2p = self.alloc(array_ty(self.n, i8), points_to = s2)         self.precondition(cryptol(f\"{s1.name()} == {s2.name()}\"))          self.execute_func(s1p, s2p, cryptol(f\"{self.n} : [64]\"))          self.returns(cryptol(\"0 : [32]\"))<\/code><\/pre>\n<p>\u041f\u0440\u0435\u0434\u0432\u0430\u0440\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u043c\u0438 \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u043c\u0438 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043d\u0430\u043b\u0438\u0447\u0438\u0435 \u0434\u0432\u0443\u0445 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432 (s1p \u0438&nbsp;s2p), \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 s1 \u0438&nbsp;s2&nbsp;\u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u043e. \u0412&nbsp;\u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u043e\u0441\u0442\u044c \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0433\u043e \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u0435\u0442 \u0432\u044b\u0437\u043e\u0432 self.precondition(&#8230;). \u0410\u0440\u0433\u0443\u043c\u0435\u043d\u0442 self.precondition(&#8230;) \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u043d\u0430&nbsp;<a href=\"https:\/\/cryptol.net\/\">Cryptol<\/a>, \u043f\u0440\u0435\u0434\u043c\u0435\u0442\u043d\u043e-\u043e\u0440\u0438\u0435\u043d\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f (DSL), \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u043e\u043c \u0432&nbsp;\u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0438. \u041f\u0440\u0438\u0432\u0435\u0434\u0451\u043d\u043d\u043e\u0435 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0435 \u043d\u0430&nbsp;Cryptol \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043f\u0440\u043e\u0441\u0442\u043e\u0435, \u0442\u0430\u043a \u043a\u0430\u043a \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442 \u0442\u043e\u043b\u044c\u043a\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0443 \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430, \u043d\u043e&nbsp;\u043d\u0438\u0436\u0435 \u043c\u044b&nbsp;\u0443\u0432\u0438\u0434\u0438\u043c \u0431\u043e\u043b\u0435\u0435 \u0441\u043b\u043e\u0436\u043d\u044b\u0435 \u043f\u0440\u0438\u043c\u0435\u0440\u044b \u043d\u0430&nbsp;Cryptol.<\/p>\n<p>\u0410\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430\u043c\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0434\u0432\u0430 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u0430 \u0441&nbsp;\u0443\u043a\u0430\u0437\u0430\u043d\u0438\u0435\u043c \u0438\u0445&nbsp;\u0434\u043b\u0438\u043d (self.n), \u043f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u0443\u0435\u043c\u044b\u0445 \u0432\u043d\u0430\u0447\u0430\u043b\u0435 \u0432&nbsp;\u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0435 Cryptol, \u0447\u0442\u043e\u0431\u044b SAW \u043c\u043e\u0433 \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u043e&nbsp;\u043d\u0438\u0445 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435. \u041f\u043e\u0440\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0435, \u0441\u043d\u043e\u0432\u0430 \u0432&nbsp;\u0432\u0438\u0434\u0435 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u043d\u0430&nbsp;Cryptol, \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432&nbsp;\u0442\u043e\u043c, \u0447\u0442\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 0.<\/p>\n<p>\u041f\u043e\u0441\u043b\u0435 \u043f\u0440\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u044f \u0432\u0441\u0435\u0439 \u043f\u043e\u0434\u0433\u043e\u0442\u043e\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0440\u0430\u0431\u043e\u0442\u044b \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c, \u0447\u0442\u043e signal_constant_memcmp \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0441\u043e\u0437\u0434\u0430\u043d\u043d\u043e\u0439 \u043d\u0430\u043c\u0438 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438:<\/p>\n<pre><code class=\"python\">mod = llvm_load_module(\"libsignal-protocol-c.bc\") # An LLVM bitcode file array_len = 42 # Pick whichever length you want to check llvm_verify(mod, \"signal_constant_memcmp\",  ConstantMemcmpEqualSpec(array_len))<\/code><\/pre>\n<p>\u0415\u0441\u043b\u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u043f\u0440\u043e\u0439\u0434\u0451\u0442 \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e, \u043c\u043e\u0436\u043d\u043e \u0437\u0430\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u044d\u0442\u043e\u0442 \u043a\u043e\u0434 \u043d\u0430&nbsp;Python \u0438&nbsp;\u0443\u0432\u0438\u0434\u0435\u0442\u044c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442:<\/p>\n<pre><code>Verified: lemma_ConstantMemcmpEqualSpec (defined at signal_protocol.py:122)<\/code><\/pre>\n<p>\u0423\u0440\u0430! \u0418\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442 SAW \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u043b \u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0431\u043e\u0442\u044b \u0443\u0442\u0438\u043b\u0438\u0442\u044b signal_constant_memcmp. \u0412\u0430\u0436\u043d\u043e \u043e\u0442\u043c\u0435\u0442\u0438\u0442\u044c, \u0447\u0442\u043e \u043d\u0430\u043c \u043d\u0435&nbsp;\u043d\u0443\u0436\u043d\u043e \u0431\u044b\u043b\u043e \u0434\u0430\u0436\u0435 \u0443\u043f\u043e\u043c\u0438\u043d\u0430\u0442\u044c \u043e&nbsp;\u0431\u0438\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u043d\u0438\u043f\u0443\u043b\u044f\u0446\u0438\u044f\u0445 \u0432\u043d\u0443\u0442\u0440\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438&nbsp;\u2014 SAW \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043b \u0438\u0445&nbsp;\u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438. \u041e\u0442\u043c\u0435\u0442\u0438\u043c, \u043e\u0434\u043d\u0430\u043a\u043e, \u0447\u0442\u043e \u043a\u043e\u043c\u0430\u043d\u0434\u0430 ConstantMemcmpEqualSpec \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u0442 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u044f\u0449\u0435\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u0432&nbsp;\u0442\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435, \u0435\u0441\u043b\u0438 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0435 \u043c\u0430\u0441\u0441\u0438\u0432\u044b \u0440\u0430\u0432\u043d\u044b \u0434\u0440\u0443\u0433 \u0434\u0440\u0443\u0433\u0443. \u0415\u0441\u043b\u0438&nbsp;\u0431\u044b \u043c\u044b&nbsp;\u0445\u043e\u0442\u0435\u043b\u0438 \u043e\u0445\u0430\u0440\u0430\u043a\u0442\u0435\u0440\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u044f\u0449\u0435\u0435 \u0432&nbsp;\u0441\u043b\u0443\u0447\u0430\u0435 \u043d\u0435\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432, \u043f\u043e\u0442\u0440\u0435\u0431\u043e\u0432\u0430\u043b\u0430\u0441\u044c&nbsp;\u0431\u044b \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0431\u043e\u043b\u0435\u0435 \u0441\u043b\u043e\u0436\u043d\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f.<\/p>\n<p>\u0422\u0430\u043a\u0436\u0435 \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u043e\u0442\u043c\u0435\u0442\u0438\u0442\u044c, \u0447\u0442\u043e \u0432&nbsp;\u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d\u043d\u043e\u043c \u0432\u044b\u0448\u0435 \u043a\u043e\u0434\u0435 \u0432\u0441\u0442\u0440\u0435\u0447\u0430\u044e\u0442\u0441\u044f \u043f\u043e\u0432\u0442\u043e\u0440\u0435\u043d\u0438\u044f, \u0442\u0430\u043a \u043a\u0430\u043a \u043c\u044b&nbsp;\u0434\u0432\u0430\u0436\u0434\u044b \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u043c \u0444\u0443\u043d\u043a\u0446\u0438\u044e self.fresh_var(), \u0430&nbsp;\u0437\u0430\u0442\u0435\u043c self.alloc(). \u041a&nbsp;\u0441\u0447\u0430\u0441\u0442\u044c\u044e, Python \u0438\u0437\u0431\u0430\u0432\u043b\u044f\u0435\u0442 \u043e\u0442&nbsp;\u0442\u0430\u043a\u0438\u0445 \u043f\u0440\u043e\u0431\u043b\u0435\u043c:<\/p>\n<pre><code class=\"python\">def ptr_to_fresh(spec: Contract, ty: LLVMType,                  name: str) -&gt; Tuple[FreshVar, SetupVal]:     var = spec.fresh_var(ty, name)     ptr = spec.alloc(ty, points_to = var)     return (var, ptr)  class ConstantMemcmpEqualSpec(Contract):     ...      def specification(self) -&gt; None:         (s1, s1p) = ptr_to_fresh(self, array_ty(self.n, i8), \"s1\")         (s2, s2p) = ptr_to_fresh(self, array_ty(self.n, i8), \"s2\")         ...<\/code><\/pre>\n<h3>\u0412\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043a\u043e\u0434\u0430 \u0441&nbsp;\u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c HMAC<\/h3>\n<p>\u041e\u0442&nbsp;\u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 libsignal-protocol-c \u0442\u0440\u0435\u0431\u0443\u0435\u0442\u0441\u044f \u0433\u043e\u0440\u0430\u0437\u0434\u043e \u0431\u043e\u043b\u044c\u0448\u0435, \u0447\u0435\u043c \u043f\u0440\u043e\u0441\u0442\u043e \u0445\u0440\u0430\u043d\u0438\u0442\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f&nbsp;\u2014 \u043e\u043d\u0430 \u0442\u0430\u043a\u0436\u0435 \u0434\u043e\u043b\u0436\u043d\u0430 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0442\u044c \u0438&nbsp;\u043f\u043e\u043b\u0443\u0447\u0430\u0442\u044c&nbsp;\u0438\u0445. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0448\u0438\u0444\u0440\u043e\u0432\u0430\u0442\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0442\u0430\u043a, \u0447\u0442\u043e\u0431\u044b \u0438\u0445&nbsp;\u043c\u043e\u0433 \u043f\u0440\u043e\u0447\u0438\u0442\u0430\u0442\u044c \u0442\u043e\u043b\u044c\u043a\u043e \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u0435\u043c\u044b\u0439 \u043f\u043e\u043b\u0443\u0447\u0430\u0442\u0435\u043b\u044c, \u0447\u0442\u043e\u0431\u044b \u0447\u0430\u0441\u0442\u043d\u0443\u044e \u043f\u0435\u0440\u0435\u043f\u0438\u0441\u043a\u0443 \u043d\u0435&nbsp;\u043c\u043e\u0433\u043b\u0438 \u043f\u0435\u0440\u0435\u0445\u0432\u0430\u0442\u0438\u0442\u044c \u0442\u0440\u0435\u0442\u044c\u0438 \u043b\u0438\u0446\u0430.<\/p>\n<p>\u041e\u0434\u043d\u0438\u043c \u0438\u0437&nbsp;\u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0445 \u044d\u0442\u0430\u043f\u043e\u0432 \u0448\u0438\u0444\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043f\u0440\u0438\u0441\u043e\u0435\u0434\u0438\u043d\u0435\u043d\u0438\u0435 <em>\u043a\u043e\u0434\u0430 \u0430\u0443\u0442\u0435\u043d\u0442\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f<\/em> (MAC), \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043f\u043e\u0441\u043b\u0435 \u043e\u0442\u043f\u0440\u0430\u0432\u043a\u0438 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0435\u0433\u043e \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u043d\u0435&nbsp;\u043c\u0435\u043d\u044f\u043b\u043e\u0441\u044c. \u0412&nbsp;\u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, libsignal-protocol-c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442 <a href=\"https:\/\/en.wikipedia.org\/wiki\/HMAC\">HMAC<\/a>, \u0442\u0438\u043f MAC, \u0432\u044b\u0447\u0438\u0441\u043b\u044f\u0435\u043c\u044b\u0439 \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0445\u0435\u0448-\u0444\u0443\u043d\u043a\u0446\u0438\u0438.<\/p>\n<p>\u041f\u043e\u0434\u0440\u043e\u0431\u043d\u043e\u0435 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u0440\u0430\u0431\u043e\u0442\u044b HMAC&nbsp;\u2014 \u0442\u0435\u043c\u0430 \u0434\u043b\u044f \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0438. \u041d\u043e, \u043a&nbsp;\u0441\u0447\u0430\u0441\u0442\u044c\u044e, \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 SAW, \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u043e\u0439 \u0441&nbsp;HMAC, \u043d\u0435&nbsp;\u043d\u0443\u0436\u043d\u043e \u0432\u0434\u0430\u0432\u0430\u0442\u044c\u0441\u044f \u0432&nbsp;\u0434\u0435\u0442\u0430\u043b\u0438. \u0412\u043c\u0435\u0441\u0442\u043e \u044d\u0442\u043e\u0433\u043e \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c <em>\u043d\u0435\u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0438\u0440\u0443\u0435\u043c\u044b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438<\/em>. \u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u0441\u043e\u0437\u0434\u0430\u0434\u0438\u043c \u0440\u044f\u0434 \u0444\u0443\u043d\u043a\u0446\u0438\u0439 Cryptol, \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0449\u0438\u0445 \u0445\u0430\u0440\u0430\u043a\u0442\u0435\u0440 \u0440\u0430\u0431\u043e\u0442\u044b HMAC:<\/p>\n<pre><code class=\"haskell\">hmac_init : {n} [n][8] -&gt; HMACContext hmac_init = undefined  hmac_update : {n} [n][8] -&gt; HMACContext -&gt; HMACContext hmac_update = undefined  hmac_final : HMACContext -&gt; [SIGNAL_MESSAGE_MAC_LENGTH][8] hmac_final = undefined<\/code><\/pre>\n<p>\u042d\u0442\u043e \u0431\u0443\u0434\u0443\u0442 \u043d\u0435\u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0438\u0440\u0443\u0435\u043c\u044b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0435 \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u043a\u043e\u0434\u0430, \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u043e\u0433\u043e \u0441&nbsp;HMAC, \u0432&nbsp;\u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 libsignal-protocol-c. \u041e\u0441\u043d\u043e\u0432\u043d\u0430\u044f \u0438\u0434\u0435\u044f \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432&nbsp;\u0442\u043e\u043c, \u0447\u0442\u043e, \u043f\u043e\u043b\u0443\u0447\u0438\u0432 \u043d\u0430&nbsp;\u0432\u0445\u043e\u0434\u0435 \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u043a\u043b\u044e\u0447, hmac_init \u0441\u043e\u0437\u0434\u0430\u0441\u0442 HMACContext. HMACContext \u0431\u0443\u0434\u0435\u0442 \u043c\u043d\u043e\u0433\u043e\u043a\u0440\u0430\u0442\u043d\u043e \u043e\u0431\u043d\u043e\u0432\u043b\u044f\u0442\u044c\u0441\u044f \u0447\u0435\u0440\u0435\u0437 hmac_update, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u0434\u0430\u043d\u043d\u044b\u0435 \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430. \u0417\u0430\u0442\u0435\u043c hmac_final \u043f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u0443\u0435\u0442 HMACContext \u0432&nbsp;signal_buffer \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0439 \u0434\u043b\u0438\u043d\u044b \u0434\u043b\u044f \u0445\u0440\u0430\u043d\u0435\u043d\u0438\u044f MAC.<\/p>\n<p>\u041e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 HMACContext \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442&nbsp;\u0442\u043e\u0433\u043e, \u043a\u0430\u043a\u0430\u044f \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0430\u044f \u0445\u044d\u0448-\u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0432&nbsp;\u0441\u043e\u0447\u0435\u0442\u0430\u043d\u0438\u0438 \u0441&nbsp;HMAC. \u041f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u044b \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 libsignal-protocol-c \u043d\u0430\u0441\u0442\u0440\u043e\u0435\u043d\u044b \u0434\u043b\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0445 \u0435\u044e&nbsp;\u0445\u0435\u0448-\u0444\u0443\u043d\u043a\u0446\u0438\u0439, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043c\u043e\u0436\u043d\u043e \u0441\u0432\u043e\u0431\u043e\u0434\u043d\u043e \u043f\u043e\u0434\u043a\u043b\u044e\u0447\u0430\u0442\u044c \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 <a href=\"https:\/\/www.openssl.org\/\">OpenSSL<\/a>, <a href=\"https:\/\/developer.apple.com\/library\/archive\/documentation\/System\/Conceptual\/ManPages_iPhoneOS\/man3\/Common%20Crypto.3cc.html\">Common Crypto<\/a> \u0438\u043b\u0438 \u0434\u0440\u0443\u0433\u0443\u044e \u043f\u043e\u0434\u0445\u043e\u0434\u044f\u0449\u0443\u044e \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0443.<\/p>\n<p>\u041f\u043e\u0441\u043a\u043e\u043b\u044c\u043a\u0443 \u044d\u0442\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0441\u0447\u0438\u0442\u0430\u044e\u0442\u0441\u044f \u043d\u0435\u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0438\u0440\u0443\u0435\u043c\u044b\u043c\u0438, SAW \u043d\u0435&nbsp;\u0431\u0443\u0434\u0435\u0442 \u0438\u0445&nbsp;\u043e\u0446\u0435\u043d\u0438\u0432\u0430\u0442\u044c \u0432\u043e&nbsp;\u0432\u0440\u0435\u043c\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438. \u0414\u0440\u0443\u0433\u0438\u043c\u0438 \u0441\u043b\u043e\u0432\u0430\u043c\u0438, \u0442\u043e, \u043a\u0430\u043a \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u044b \u044d\u0442\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u043d\u0435&nbsp;\u0438\u043c\u0435\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f; undefined \u0432\u044b\u0431\u0440\u0430\u043d\u043e \u0434\u043b\u044f \u0443\u0434\u043e\u0431\u0441\u0442\u0432\u0430, \u043d\u043e&nbsp;\u043f\u043e\u0434\u043e\u0439\u0434\u0451\u0442 \u0438&nbsp;\u043b\u044e\u0431\u0430\u044f \u0434\u0440\u0443\u0433\u0430\u044f \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f.<\/p>\n<p>\u041f\u043e\u0441\u043b\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u044f \u044d\u0442\u0438\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u0439 \u043c\u043e\u0436\u043d\u043e \u0441\u0432\u044f\u0437\u0430\u0442\u044c \u0438\u0445&nbsp;\u0441&nbsp;\u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u044e\u0449\u0438\u043c\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044f\u043c\u0438 C&nbsp;\u0432&nbsp;\u0441\u0430\u043c\u043e\u0439 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435. \u041d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, \u0432\u043e\u0442 \u0441\u043e\u043a\u0440\u0430\u0449\u0451\u043d\u043d\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0434\u043b\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\/blob\/3a83a4f4ed2302ff6e68ab569c88793b50c22d28\/src\/signal_protocol.c#L464-L469\">signal_hmac_sha256_initC<\/a>:<\/p>\n<pre><code class=\"python\">class SignalHmacSha256InitSpec(Contract):     key_len: int      def specification(self) -&gt; None:         hmac_context_ptr = self.alloc(...)         (key_data, key)  = ptr_to_fresh(self, array_ty(self.key_len, i8),                                         \"key_data\")    \t          self.execute_func(..., hmac_context_ptr, key,                           cryptol(f\"{self.key_len} : [64]\"))          init = f\"hmac_init`{{ {self.key_len} }} {key_data.name()}\"         dummy_hmac_context = self.alloc(..., points_to = cryptol(init))         self.points_to(hmac_context_ptr, dummy_hmac_context)         self.returns(cryptol(\"0 : [32]\"))   key_len = 32 init_spec = llvm_assume(mod, \"signal_hmac_sha256_init\",                         SignalHmacSha256InitSpec(key_len))<\/code><\/pre>\n<p>\u041d\u0435&nbsp;\u0441\u0442\u0430\u0440\u0430\u0439\u0442\u0435\u0441\u044c \u043f\u043e\u043d\u044f\u0442\u044c \u043a\u0430\u0436\u0434\u0443\u044e \u0441\u0442\u0440\u043e\u0447\u043a\u0443 \u043a\u043e\u0434\u0430. \u041f\u0440\u043e\u0441\u0442\u043e \u0437\u043d\u0430\u0439\u0442\u0435, \u0447\u0442\u043e \u0441\u0430\u043c\u043e\u0439 \u0432\u0430\u0436\u043d\u043e\u0439 \u0435\u0433\u043e \u0447\u0430\u0441\u0442\u044c\u044e \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u044f\u044f \u0441\u0442\u0440\u043e\u043a\u0430, \u0432&nbsp;\u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0432\u043c\u0435\u0441\u0442\u043e llvm_verify \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f llvm_assume. \u0424\u0443\u043d\u043a\u0446\u0438\u044f llvm_assume \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 SAW \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e, \u0444\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u043d\u0435&nbsp;\u043c\u043e\u0434\u0435\u043b\u0438\u0440\u0443\u044f \u0435\u0451&nbsp;\u2014 \u043f\u043e&nbsp;\u0441\u0443\u0442\u0438 SAW \u0442\u0440\u0430\u043a\u0442\u0443\u0435\u0442 \u0435\u0451&nbsp;\u043a\u0430\u043a \u0430\u043a\u0441\u0438\u043e\u043c\u0443. \u042d\u0442\u043e \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u043f\u0440\u0438\u0432\u044f\u0437\u0430\u0442\u044c \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 signal_hmac_sha256_init \u043a&nbsp;\u043d\u0435\u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0438\u0440\u0443\u0435\u043c\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 hmac_init \u0432&nbsp;\u043f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u044f\u0445 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438.<\/p>\n<p>\u0410\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u044b\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c llvm_assume \u0442\u0430\u043a\u0436\u0435 \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0439, \u0432\u043a\u043b\u044e\u0447\u0430\u044e\u0449\u0438\u0445 hmac_update \u0438&nbsp;hmac_final. \u041f\u043e\u0441\u043b\u0435 \u044d\u0442\u043e\u0433\u043e \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c \u043e\u0447\u0435\u043d\u044c \u0432\u0430\u0436\u043d\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e, \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u0443\u044e \u0441&nbsp;MAC: <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\/blob\/3a83a4f4ed2302ff6e68ab569c88793b50c22d28\/src\/protocol.c%23L377-L518\">signal_message_verify_mac<\/a>. \u0424\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0434\u0430\u043d\u043d\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u0432&nbsp;\u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430, \u0432\u044b\u0447\u0438\u0441\u043b\u044f\u0435\u0442 MAC \u0434\u043b\u044f \u0434\u0430\u043d\u043d\u044b\u0445 \u0432\u043d\u0443\u0442\u0440\u0438 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0438&nbsp;\u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442, \u0441\u043e\u0432\u043f\u0430\u0434\u0430\u0435\u0442&nbsp;\u043b\u0438 \u043e\u043d&nbsp;\u0441&nbsp;MAC \u0432&nbsp;\u043a\u043e\u043d\u0446\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f. \u0415\u0441\u043b\u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0441\u043e\u0432\u043f\u0430\u0434\u0430\u044e\u0442, \u043c\u043e\u0436\u043d\u043e \u0441&nbsp;\u0443\u0432\u0435\u0440\u0435\u043d\u043d\u043e\u0441\u0442\u044c\u044e \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0430\u0442\u044c, \u0447\u0442\u043e \u043f\u0440\u0438 \u043e\u0442\u043f\u0440\u0430\u0432\u043a\u0435 \u043f\u043e\u043b\u0443\u0447\u0430\u0442\u0435\u043b\u044e \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u043d\u0435&nbsp;\u043c\u0435\u043d\u044f\u043b\u043e\u0441\u044c.<\/p>\n<p>\u041e\u0431\u044a\u044f\u0441\u043d\u0435\u043d\u0438\u0435 \u0432\u0441\u0435\u0445 \u0442\u043e\u043d\u043a\u043e\u0441\u0442\u0435\u0439 \u0440\u0430\u0431\u043e\u0442\u044b signal_message_verify_mac \u0437\u0430\u043d\u044f\u043b\u043e&nbsp;\u0431\u044b \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043c\u043d\u043e\u0433\u043e \u0432\u0440\u0435\u043c\u0435\u043d\u0438, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0432&nbsp;\u044d\u0442\u043e\u0439 \u0437\u0430\u043c\u0435\u0442\u043a\u0435 \u043c\u044b&nbsp;\u043a\u043e\u0441\u043d\u0451\u043c\u0441\u044f \u043b\u0438\u0448\u044c \u0433\u043b\u0430\u0432\u043d\u043e\u0433\u043e \u0432\u043e\u043f\u0440\u043e\u0441\u0430: \u043a\u0430\u043a \u0434\u043e\u043b\u0436\u043d\u043e \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u0442\u044c \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f? \u0414\u0430\u043d\u043d\u044b\u0435 \u0432\u043d\u0443\u0442\u0440\u0438 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u043c\u043e\u0433\u0443\u0442 \u0431\u044b\u0442\u044c \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u043b\u044c\u043d\u044b\u043c\u0438, \u043e\u0434\u043d\u0430\u043a\u043e MAC \u0432&nbsp;\u043a\u043e\u043d\u0446\u0435 \u0434\u043e\u043b\u0436\u0435\u043d \u0438\u043c\u0435\u0442\u044c \u0432\u043f\u043e\u043b\u043d\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0451\u043d\u043d\u0443\u044e \u0444\u043e\u0440\u043c\u0443. \u042d\u0442\u0443 \u0444\u043e\u0440\u043c\u0443 \u043c\u043e\u0436\u043d\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u0438 Python:<\/p>\n<pre><code class=\"python\">def mk_hmac(serialized_len: int, serialized_data: FreshVar,         \treceiver_identity_key_data : FreshVar,         \tsender_identity_key_data: FreshVar,         \tmac_key_len: int, mac_key_data: FreshVar) -&gt; SetupVal:     sender_identity_buf = f\"\"\"         [{DJB_TYPE}] # {sender_identity_key_data.name()}             : [{DJB_KEY_LEN} + 1][8]         \"\"\"     receiver_identity_buf = f\"\"\"         [{DJB_TYPE}] # {receiver_identity_key_data.name()}             : [{DJB_KEY_LEN} + 1][8]         \"\"\"     hmac = f\"\"\"         hmac_final          (hmac_update`{{ {serialized_len} }} {serialized_data.name()}           (hmac_update`{{ {DJB_KEY_LEN}+1 }} ({receiver_identity_buf})            (hmac_update`{{ {DJB_KEY_LEN}+1 }} ({sender_identity_buf})             (hmac_init`{{ {mac_key_len} }} {mac_key_data.name()}))))         \"\"\"     return cryptol(hmac)<\/code><\/pre>\n<p>\u0414\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u0441\u043b\u043e\u0436\u043d\u043e, \u043d\u0435&nbsp;\u043f\u0440\u0430\u0432\u0434\u0430&nbsp;\u043b\u0438? \u041d\u043e&nbsp;\u0435\u0449\u0451 \u0440\u0430\u0437&nbsp;\u2014 \u043d\u0435&nbsp;\u0441\u0442\u0430\u0440\u0430\u0439\u0442\u0435\u0441\u044c \u043f\u043e\u043d\u044f\u0442\u044c \u043a\u0430\u0436\u0434\u0443\u044e \u0441\u0442\u0440\u043e\u0447\u043a\u0443 \u043a\u043e\u0434\u0430. \u0422\u0443\u0442 \u0432\u0430\u0436\u043d\u043e \u043f\u043e\u043d\u044f\u0442\u044c, \u0447\u0442\u043e \u0441\u043d\u0430\u0447\u0430\u043b\u0430 \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f hmac_init, \u0437\u0430\u0442\u0435\u043c \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u044e\u0442\u0441\u044f \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0432\u044b\u0437\u043e\u0432\u043e\u0432 hmac_update, \u043f\u043e\u0441\u043b\u0435 \u0447\u0435\u0433\u043e \u043e\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0432\u044b\u0437\u043e\u0432 hmac_finalcall. \u042d\u0442\u043e \u0432\u0435\u0441\u044c\u043c\u0430 \u0431\u043b\u0438\u0437\u043a\u043e \u0438\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u044b\u043c \u0434\u043e\u043f\u0443\u0449\u0435\u043d\u0438\u044f\u043c, \u0441\u0434\u0435\u043b\u0430\u043d\u043d\u044b\u043c \u0440\u0430\u043d\u0435\u0435 \u0434\u043b\u044f HMAC, \u043f\u043e\u044d\u0442\u043e\u043c\u0443, \u0435\u0441\u043b\u0438 SAW \u0443\u0431\u0435\u0434\u0438\u0442\u0441\u044f \u0432&nbsp;\u0442\u043e\u043c, \u0447\u0442\u043e MAC \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u043a\u0430\u043a \u0434\u0430\u043d\u043d\u043e\u0435 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0435 Cryptol, \u043c\u043e\u0436\u043d\u043e \u0431\u044b\u0442\u044c \u0443\u0432\u0435\u0440\u0435\u043d\u043d\u044b\u043c, \u0447\u0442\u043e \u043e\u043d&nbsp;\u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0442\u0430\u043a, \u043a\u0430\u043a \u043e\u0436\u0438\u0434\u0430\u043b\u043e\u0441\u044c.<\/p>\n<p>\u0414\u0430\u043b\u0435\u0435 \u043d\u0430\u043c \u043d\u0443\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u044d\u0442\u043e \u0432&nbsp;\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438. \u0412\u043e\u0442 \u0432\u044b\u0434\u0435\u0440\u0436\u043a\u0430 \u0438\u0437&nbsp;\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0434\u043b\u044f signal_message_verify_mac, \u0432&nbsp;\u043a\u043e\u0442\u043e\u0440\u043e\u0439 \u0432&nbsp;\u043f\u0440\u0435\u0434\u0443\u0441\u043b\u043e\u0432\u0438\u044f\u0445 \u043e\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442\u0441\u044f, \u043a\u0430\u043a \u0434\u043e\u043b\u0436\u043d\u043e \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u0442\u044c \u0432\u0430\u043b\u0438\u0434\u043d\u043e\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435:<\/p>\n<pre><code class=\"python\">lass SignalMessageVerifyMacSpec(Contract):     serialized_len: int      def specification(self) -&gt; None:         ...         mac_index = 8 + self.serialized_len - SIGNAL_MESSAGE_MAC_LENGTH         ser_len   = f\"{self.serialized_len} : [64]\"          self.points_to(serialized[0], cryptol(ser_len))         self.points_to(serialized[8], serialized_message_data)         self.points_to(serialized[mac_index], mk_hmac(...))          self.execute_func(...)          self.returns(cryptol(\"1 : [32]\"))<\/code><\/pre>\n<p>\u0417\u0434\u0435\u0441\u044c serialized \u0443\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442 \u043d\u0430&nbsp;signal_buffer \u0434\u043b\u044f \u0432\u0441\u0435\u0433\u043e \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f. \u0414\u043b\u044f \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u044f \u043f\u0430\u043c\u044f\u0442\u0438, \u0441\u043e\u0434\u0435\u0440\u0436\u0430\u0449\u0435\u0439\u0441\u044f \u0432&nbsp;\u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0445 \u0447\u0430\u0441\u0442\u044f\u0445 \u0431\u0443\u0444\u0435\u0440\u0430, \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u043d\u043e\u0442\u0430\u0446\u0438\u044e \u0441\u043b\u0430\u0439\u0441\u0430 Python (\u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440, serialized[0]). \u041f\u0435\u0440\u0432\u0430\u044f \u0447\u0430\u0441\u0442\u044c \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 self.serialized_len, \u043e\u0431\u0449\u0443\u044e \u0434\u043b\u0438\u043d\u0443 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f. \u0427\u0435\u0440\u0435\u0437 \u0432\u043e\u0441\u0435\u043c\u044c \u0431\u0430\u0439\u0442&nbsp;\u0440\u0430\u0437\u043c\u0435\u0449\u0430\u0435\u0442\u0441\u044f serialized_message_data&nbsp;\u2014 \u0434\u0430\u043d\u043d\u044b\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f. \u0412&nbsp;\u0441\u0430\u043c\u043e\u043c \u043a\u043e\u043d\u0446\u0435 \u0431\u0443\u0444\u0435\u0440\u0430 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442\u0441\u044f MAC, \u0432\u044b\u0447\u0438\u0441\u043b\u0435\u043d\u043d\u044b\u0439 \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e mk_hmac(&#8230;).<\/p>\n<p>\u041f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c \u0432\u0441\u0451 \u043d\u0430&nbsp;\u043f\u0440\u0430\u043a\u0442\u0438\u043a\u0435&nbsp;\u2014 \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u043c llvm_verify \u0441\u043e\u0433\u043b\u0430\u0441\u043d\u043e \u044d\u0442\u043e\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438. \u0412&nbsp;\u044d\u0442\u043e\u0442 \u0440\u0430\u0437 \u043d\u0443\u0436\u043d\u043e \u043f\u0435\u0440\u0435\u0434\u0430\u0442\u044c \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0445 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u0432. \u041d\u0443\u0436\u043d\u043e \u044f\u0432\u043d\u043e \u0443\u043a\u0430\u0437\u0430\u0442\u044c, \u043a\u0430\u043a\u0438\u0435 \u0434\u043e\u043f\u0443\u0449\u0435\u043d\u0438\u044f \u043c\u044b&nbsp;\u0441\u0434\u0435\u043b\u0430\u043b\u0438 \u0440\u0430\u043d\u0435\u0435 \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e llvm_assume \u043f\u043e\u0441\u0440\u0435\u0434\u0441\u0442\u0432\u043e\u043c \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430 lemmas. \u0422\u0430\u043a\u0436\u0435 \u043d\u0443\u0436\u043d\u043e \u0443\u043a\u0430\u0437\u0430\u0442\u044c \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u0443 \u0440\u0435\u0448\u0435\u043d\u0438\u044f SMT, \u043a\u0430\u043a\u0438\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0434\u043e\u043b\u0436\u043d\u044b \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0442\u044c\u0441\u044f \u043a\u0430\u043a \u043d\u0435\u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0438\u0440\u0443\u0435\u043c\u044b\u0435. \u042d\u0442\u043e \u0434\u0435\u043b\u0430\u0435\u0442\u0441\u044f \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430 script:<\/p>\n<pre><code class=\"python\">uninterps = [\"hmac_init\", \"hmac_update\", \"hmac_final\"] llvm_verify(mod, \"signal_message_verify_mac\",  SignalMessageVerifyMacSpec(...),             lemmas=[init_spec, update_spec1, update_spec2, final_spec],             script=ProofScript([z3(uninterps)]))<\/code><\/pre>\n<p>\u0412 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 \u043c\u044b \u0432\u0438\u0434\u0438\u043c \u0434\u043e\u043b\u0433\u043e\u0436\u0434\u0430\u043d\u043d\u0443\u044e \u0437\u0435\u043b\u0451\u043d\u0443\u044e \u0433\u0430\u043b\u043e\u0447\u043a\u0443:<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/3b0\/ce4\/9af\/3b0ce49af134b73eb791137f7b7b4b04.png\" width=\"633\" height=\"39\"><figcaption><\/figcaption><\/figure>\n<h3>\u041f\u043b\u0430\u043d\u044b<\/h3>\n<p>\u0421&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e saw-client \u043c\u044b&nbsp;\u0441\u043c\u043e\u0433\u043b\u0438 \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0440\u044f\u0434 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u044b\u0445 \u0434\u0430\u043d\u043d\u044b\u0445 \u043e&nbsp;\u043a\u043e\u0434\u0435 \u0432&nbsp;libsignal-protocol-c. \u041c\u044b&nbsp;\u0441\u043c\u043e\u0433\u043b\u0438 \u043f\u0440\u043e\u0434\u0435\u043c\u043e\u043d\u0441\u0442\u0440\u0438\u0440\u043e\u0432\u0430\u0442\u044c, \u0447\u0442\u043e <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\/blob\/3a83a4f4ed2302ff6e68ab569c88793b50c22d28\/src\/protocol.c%23L377-L518\">signal_message_verify_mac<\/a>, \u0444\u0443\u043d\u043a\u0446\u0438\u044f, \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u044e\u0449\u0430\u044f \u0446\u0435\u043b\u043e\u0441\u0442\u043d\u043e\u0441\u0442\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f, \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u043d\u043e\u0433\u043e \u043f\u043e&nbsp;\u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0443 Signal, \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u043e, \u0435\u0441\u043b\u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u044f\u044f \u0447\u0430\u0441\u0442\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u0442 \u0432\u0435\u0440\u043d\u044b\u0439 \u043a\u043e\u0434 \u0430\u0443\u0442\u0435\u043d\u0442\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f (MAC). \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u043c\u044b&nbsp;\u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u043b\u0438, \u043a\u0430\u043a\u0438\u043c \u0434\u043e\u043b\u0436\u043d\u043e \u0431\u044b\u0442\u044c \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 MAC \u043e\u0442\u043d\u043e\u0441\u0438\u0442\u0435\u043b\u044c\u043d\u043e \u0430\u0431\u0441\u0442\u0440\u0430\u043a\u0442\u043d\u043e\u0439 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u0445\u044d\u0448-\u0444\u0443\u043d\u043a\u0446\u0438\u0439.<\/p>\n<p>\u041e\u0434\u043d\u0430\u043a\u043e \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u0430 saw-client \u043c\u043e\u0436\u043d\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u0433\u043e\u0440\u0430\u0437\u0434\u043e \u0431\u043e\u043b\u044c\u0448\u0435, \u0447\u0435\u043c \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u0430\u043d\u043e \u0432&nbsp;\u0434\u0430\u043d\u043d\u043e\u0439 \u0437\u0430\u043c\u0435\u0442\u043a\u0435. \u041c\u044b&nbsp;\u043f\u0440\u043e\u0432\u0435\u0440\u044f\u043b\u0438 \u043a\u043b\u044e\u0447\u0435\u0432\u043e\u0435 \u0441\u0432\u043e\u0439\u0441\u0442\u0432\u043e \u043a\u043e\u0434\u0430, \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u044e\u0449\u0435\u0433\u043e \u0446\u0435\u043b\u043e\u0441\u0442\u043d\u043e\u0441\u0442\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439. \u041d\u043e&nbsp;\u0442\u0430\u043a\u0430\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u0446\u0435\u043b\u043e\u0441\u0442\u043d\u043e\u0441\u0442\u0438 \u043d\u0435&nbsp;\u043a\u0430\u0441\u0430\u043b\u0430\u0441\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u043f\u0435\u0440\u0435\u0434\u0430\u0432\u0430\u0435\u043c\u044b\u0445 \u043f\u043e&nbsp;\u043f\u0440\u043e\u0432\u043e\u0434\u0430\u043c. \u041c\u044b&nbsp;\u0442\u0430\u043a\u0436\u0435 \u043d\u0435&nbsp;\u0441\u0442\u0430\u043b\u0438 \u043f\u043e\u043b\u043d\u043e\u0441\u0442\u044c\u044e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0442\u044c \u043f\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u0435 HMAC, \u0445\u043e\u0442\u044f \u044d\u0442\u043e \u043c\u043e\u0436\u043d\u043e \u0431\u044b\u043b\u043e&nbsp;\u0431\u044b \u0441\u0434\u0435\u043b\u0430\u0442\u044c; \u0441\u043c\u043e\u0442\u0440\u0438\u0442\u0435 <a href=\"https:\/\/galois.com\/blog\/2016\/09\/verifying-s2n-hmac-with-saw\/\">\u0437\u0434\u0435\u0441\u044c<\/a>.<\/p>\n<p>\u041d\u0435\u0441\u043c\u043e\u0442\u0440\u044f \u043d\u0430&nbsp;\u0442\u043e \u0447\u0442\u043e saw-client \u043c\u043e\u0436\u0435\u0442 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c\u0441\u044f \u043a\u0430\u043a \u0441\u0430\u043c\u043e\u0441\u0442\u043e\u044f\u0442\u0435\u043b\u044c\u043d\u044b\u0439 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u0432&nbsp;\u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0430\u0441\u043f\u0435\u043a\u0442\u0430\u0445 saw-client \u043d\u0435&nbsp;\u0434\u043e\u0441\u0442\u0438\u0433\u0430\u0435\u0442 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u0438 SAWScript. saw-client \u0432&nbsp;\u043d\u0430\u0441\u0442\u043e\u044f\u0449\u0435\u0435 \u0432\u0440\u0435\u043c\u044f \u043d\u0435&nbsp;\u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0435\u0442 \u0440\u044f\u0434 \u0444\u0443\u043d\u043a\u0446\u0438\u0439 SAW, \u043d\u0430\u043f\u0440\u0438\u043c\u0435\u0440 \u0444\u0443\u043d\u043a\u0446\u0438\u044e <a href=\"https:\/\/github.com\/GaloisInc\/saw-script\/issues\/1153\">\u0438\u043d\u0438\u0446\u0438\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 <\/a>\u0433\u043b\u043e\u0431\u0430\u043b\u044c\u043d\u044b\u0445 \u043f\u0435\u0440\u0435\u043c\u0435\u043d\u043d\u044b\u0445 \u0432&nbsp;\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f\u0445. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0438\u0434\u0438\u043e\u043c\u044b SAWScript \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u044b \u0432&nbsp;saw-client \u043d\u0435&nbsp;\u0442\u0430\u043a &#171;\u043a\u0440\u0430\u0441\u0438\u0432\u043e&#187;, \u043f\u0440\u0438\u043c\u0435\u0440 \u2014 <a href=\"https:\/\/github.com\/GaloisInc\/saw-script\/issues\/1188\">\u043a\u0432\u0430\u0437\u0438\u043a\u0430\u0432\u044b\u0447\u043a\u0438<\/a> \u0432&nbsp;\u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f\u0445 Cryptol. \u041c\u044b&nbsp;\u0441\u0447\u0438\u0442\u0430\u0435\u043c, \u0447\u0442\u043e \u0441\u043e&nbsp;\u0432\u0440\u0435\u043c\u0435\u043d\u0435\u043c \u043d\u0430\u043c \u0443\u0434\u0430\u0441\u0442\u0441\u044f \u0440\u0435\u0448\u0438\u0442\u044c \u044d\u0442\u0438 \u043f\u0440\u043e\u0431\u043b\u0435\u043c\u044b.<\/p>\n<p>\u0412&nbsp;\u043f\u0435\u0440\u0441\u043f\u0435\u043a\u0442\u0438\u0432\u0435 \u043c\u044b&nbsp;\u043f\u043e\u043f\u044b\u0442\u0430\u0435\u043c\u0441\u044f \u0441\u0434\u0435\u043b\u0430\u0442\u044c Python \u043f\u043e\u043b\u043d\u043e\u043f\u0440\u0430\u0432\u043d\u044b\u043c \u044f\u0437\u044b\u043a\u043e\u043c \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0438\u044f \u043a\u043e\u0434\u0430 \u0434\u043b\u044f SAW, \u0438&nbsp;\u0434\u0430\u043d\u043d\u0430\u044f \u0440\u0430\u0431\u043e\u0442\u0430&nbsp;\u2014 \u043f\u0435\u0440\u0432\u044b\u0439 \u0448\u0430\u0433 \u0432&nbsp;\u044d\u0442\u043e\u043c \u043d\u0430\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0438. \u0412\u0435\u0441\u044c \u043a\u043e\u0434, \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u043d\u044b\u0439 \u0432&nbsp;\u044d\u0442\u043e\u0439 \u0437\u0430\u043c\u0435\u0442\u043a\u0435, \u043c\u043e\u0436\u043d\u043e \u043d\u0430\u0439\u0442\u0438 <a href=\"https:\/\/github.com\/GaloisInc\/saw-demos\/tree\/master\/demos\/signal-protocol\">\u0437\u0434\u0435\u0441\u044c<\/a>. \u0420\u0435\u043a\u043e\u043c\u0435\u043d\u0434\u0443\u0435\u043c \u0438\u0441\u043f\u044b\u0442\u0430\u0442\u044c \u0432&nbsp;\u0440\u0430\u0431\u043e\u0442\u0435 \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442 saw-client. \u041b\u044e\u0431\u044b\u0435 \u0432\u0430\u0448\u0438 \u043f\u043e\u0436\u0435\u043b\u0430\u043d\u0438\u044f \u0438&nbsp;\u043a\u043e\u043c\u043c\u0435\u043d\u0442\u0430\u0440\u0438\u0438 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0439\u0442\u0435 \u0432<a href=\"https:\/\/github.com\/GaloisInc\/saw-script\/\"> \u0442\u0440\u0435\u043a\u0435\u0440 <\/a>\u043f\u0440\u043e\u0431\u043b\u0435\u043c \u0438&nbsp;\u0432\u043e\u043f\u0440\u043e\u0441\u043e\u0432 SAW.<\/p>\n<p>\u0410 \u0435\u0441\u043b\u0438 \u0432\u0430\u043c \u0438\u043d\u0435\u0442\u0435\u0440\u0435\u0441\u0435\u043d \u043d\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u0430\u043d\u0430\u043b\u0438\u0437 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e Python, \u043d\u043e \u0438 \u0430\u043a\u0442\u0438\u0432\u043d\u0430\u044f \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0430 \u043d\u0430 \u044d\u0442\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u0432 \u043d\u0430\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u044f\u0445 \u043a\u0430\u043a \u0431\u0435\u043a\u0435\u043d\u0434\u0430, \u0442\u0430\u043a \u0438 \u0444\u0440\u043e\u043d\u0442\u0435\u043d\u0434\u0430, \u0442\u043e \u0432\u044b \u043c\u043e\u0436\u0435\u0442\u0435 \u043e\u0431\u0440\u0430\u0442\u0438\u0442\u044c \u0432\u043d\u0438\u043c\u0430\u043d\u0438\u0435 \u043d\u0430 \u043d\u0430\u0448 \u043a\u0443\u0440\u0441 <a href=\"https:\/\/skillfactory.ru\/python-fullstack-web-developer?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_FPW&amp;utm_term=regular&amp;utm_content=080621\">&#171;Fullstack-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a \u043d\u0430 Python&#187;<\/a>, \u0433\u0434\u0435 \u0442\u0430\u043a\u0436\u0435 \u0440\u0430\u0441\u0441\u043c\u0430\u0442\u0440\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u0442\u0435\u0441\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u041f\u041e \u0438 \u043c\u043d\u043e\u0433\u0438\u0435 \u0434\u0440\u0443\u0433\u0438\u0435 \u0430\u0441\u043f\u0435\u043a\u0442\u044b \u043f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u0438 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0441\u0442\u0430.<\/p>\n<figure class=\"full-width\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/habrastorage.org\/getpro\/habr\/upload_files\/04d\/590\/887\/04d5908875b62722df7f2b56a6de7bb8.png\" width=\"1000\" height=\"200\"><figcaption><\/figcaption><\/figure>\n<p><a href=\"https:\/\/skillfactory.ru\/courses\/?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_ALLCOURSES&amp;utm_term=regular&amp;utm_content=080621\">\u0423\u0437\u043d\u0430\u0439\u0442\u0435<\/a>, \u043a\u0430\u043a \u043f\u0440\u043e\u043a\u0430\u0447\u0430\u0442\u044c\u0441\u044f \u0438 \u0432 \u0434\u0440\u0443\u0433\u0438\u0445 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u043e\u0441\u0442\u044f\u0445 \u0438\u043b\u0438 \u043e\u0441\u0432\u043e\u0438\u0442\u044c \u0438\u0445 \u0441 \u043d\u0443\u043b\u044f:<\/p>\n<ul>\n<li>\n<p><a href=\"https:\/\/skillfactory.ru\/dstpro?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_DSPR&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f Data Scientist<\/a><\/p>\n<\/li>\n<li>\n<p><a href=\"https:\/\/skillfactory.ru\/dataanalystpro?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_DAPR&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f Data Analyst<\/a><\/p>\n<\/li>\n<li>\n<p><a href=\"https:\/\/skillfactory.ru\/dataengineer?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_DEA&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 \u043f\u043e Data Engineering<\/a><\/p>\n<\/li>\n<\/ul>\n<details class=\"spoiler\">\n<summary>\u0414\u0440\u0443\u0433\u0438\u0435 \u043f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u0438 \u0438 \u043a\u0443\u0440\u0441\u044b<\/summary>\n<div class=\"spoiler__content\">\n<p><strong>\u041f\u0420\u041e\u0424\u0415\u0421\u0421\u0418\u0418<\/strong><\/p>\n<ul>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/python-fullstack-web-developer?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_FPW&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f Fullstack-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a \u043d\u0430 Python<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/java?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_JAVA&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f Java-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/java-qa-engineer?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_QAJA&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f QA-\u0438\u043d\u0436\u0435\u043d\u0435\u0440 \u043d\u0430 JAVA<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/frontend?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_FR&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f Frontend-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/cybersecurity?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_HACKER&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f \u042d\u0442\u0438\u0447\u043d\u044b\u0439 \u0445\u0430\u043a\u0435\u0440<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/cplus?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_CPLUS&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f C++ \u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/game-dev?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_GAMEDEV&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f \u0420\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a \u0438\u0433\u0440 \u043d\u0430 Unity<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/webdev?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_WEBDEV&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f \u0412\u0435\u0431-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/iosdev?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_IOSDEV&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f iOS-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a \u0441 \u043d\u0443\u043b\u044f<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/android?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_ANDR&amp;utm_term=regular&amp;utm_content=080621\">\u041f\u0440\u043e\u0444\u0435\u0441\u0441\u0438\u044f Android-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u0447\u0438\u043a \u0441 \u043d\u0443\u043b\u044f<\/a><\/p>\n<\/li>\n<\/ul>\n<p><strong>\u041a\u0423\u0420\u0421\u042b<\/strong><\/p>\n<ul>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/ml-programma-machine-learning-online?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_ML&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 \u043f\u043e Machine Learning<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/ml-and-dl?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_MLDL&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 &#171;Machine Learning \u0438 Deep Learning&#187;<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/math-stat-for-ds#syllabus?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_MAT&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 &#171;\u041c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430 \u0434\u043b\u044f Data Science&#187;<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/math_and_ml?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_MATML&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 &#171;\u041c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u043a\u0430 \u0438 Machine Learning \u0434\u043b\u044f Data Science&#187;<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/python-for-web-developers?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_PWS&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 &#171;Python \u0434\u043b\u044f \u0432\u0435\u0431-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0438&#187;<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/algo?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_algo&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 &#171;\u0410\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u044b \u0438 \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u044b \u0434\u0430\u043d\u043d\u044b\u0445&#187;<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/analytics?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_SDA&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 \u043f\u043e \u0430\u043d\u0430\u043b\u0438\u0442\u0438\u043a\u0435 \u0434\u0430\u043d\u043d\u044b\u0445<\/a><\/p>\n<\/li>\n<li>\n<p>  <a href=\"https:\/\/skillfactory.ru\/devops?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_DEVOPS&amp;utm_term=regular&amp;utm_content=080621\">\u041a\u0443\u0440\u0441 \u043f\u043e DevOps<\/a><\/p>\n<\/li>\n<\/ul>\n<\/div>\n<\/details>\n<\/div>\n<p> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"https:\/\/habr.com\/ru\/company\/skillfactory\/blog\/561032\/\"> https:\/\/habr.com\/ru\/company\/skillfactory\/blog\/561032\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"\n<div class=\"post__text post__text_v2\" id=\"post-content-body\">\n<figure class=\"full-width\"><figcaption><\/figcaption><\/figure>\n<p>Galois \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u043d\u0430\u0434 \u043f\u043e\u0432\u044b\u0448\u0435\u043d\u0438\u0435\u043c \u0443\u0434\u043e\u0431\u0441\u0442\u0432\u0430 <a href=\"https:\/\/saw.galois.com\/\">SAW<\/a>, \u0438\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442\u0430 \u0434\u043b\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c \u043d\u0430&nbsp;C&nbsp;\u0438&nbsp;Java, \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u043a\u043e\u0434 \u043a\u0442\u043e\u0440\u043e\u0433\u043e \u043e\u0442\u043a\u0440\u044b\u0442. \u041e\u0441\u043d\u043e\u0432\u043d\u044b\u043c \u0441\u043f\u043e\u0441\u043e\u0431\u043e\u043c \u0432\u0437\u0430\u0438\u043c\u043e\u0434\u0435\u0439\u0441\u0442\u0432\u0438\u044f \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u0435\u0439 \u0441&nbsp;SAW \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0435\u0433\u043e \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0438&nbsp;\u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u0446\u0435\u043d\u0430\u0440\u0438\u0435\u0432. \u0427\u0442\u043e\u0431\u044b \u0441\u0434\u0435\u043b\u0430\u0442\u044c SAW \u043a\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u0431\u043e\u043b\u0435\u0435 \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u043c, \u0432&nbsp;\u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u044f\u0437\u044b\u043a\u0430 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f SAW \u0442\u0435\u043f\u0435\u0440\u044c \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c Python! \u0414\u043b\u044f \u0434\u0435\u043c\u043e\u043d\u0441\u0442\u0440\u0430\u0446\u0438\u0438 \u044d\u0442\u043e\u0439 \u043d\u043e\u0432\u043e\u0439 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u0438 \u0432 Galois&nbsp;\u0441\u043e\u0437\u0434\u0430\u043b\u0438 \u043f\u0440\u0438\u043c\u0435\u0440, \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u0432 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0443 \u0447\u0430\u0441\u0442\u0438 <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\">\u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438<\/a> \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 Signal \u043d\u0430&nbsp;\u044f\u0437\u044b\u043a\u0435&nbsp;\u0421.&nbsp;\u0412 \u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, \u043a\u0430\u043a \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f SAW \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0442\u0441\u044f \u0443\u0441\u043b\u043e\u0432\u0438\u044f, \u043f\u0440\u0438 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0435 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0430 Signal \u0431\u0443\u0434\u0435\u0442 \u0443\u0441\u043f\u0435\u0448\u043d\u043e \u0430\u0443\u0442\u0435\u043d\u0442\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043e. \u041a \u0441\u0442\u0430\u0440\u0442\u0443 \u043a\u0443\u0440\u0441\u0430 \u043e <a href=\"https:\/\/skillfactory.ru\/python-for-web-developers?utm_source=infopartners&amp;utm_medium=habr&amp;utm_campaign=habr_PWS&amp;utm_term=regular&amp;utm_content=080621\">Fullstack-\u0440\u0430\u0437\u0440\u0430\u0431\u043e\u0442\u043a\u0435<\/a> \u043d\u0430 Python \u043c\u044b \u043f\u0435\u0440\u0435\u0432\u0435\u043b\u0438 \u043c\u0430\u0442\u0435\u0440\u0438\u0430\u043b \u043e\u0431 \u044d\u0442\u043e\u043c \u043f\u0440\u0438\u043c\u0435\u0440\u0435.<\/p>\n<hr>\n<h3>SAW-\u043a\u043b\u0438\u0435\u043d\u0442 Python<\/h3>\n<p>\u0423\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 SAW \u043c\u043e\u0436\u0435\u0442 \u043e\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043b\u044f\u0442\u044c\u0441\u044f \u0441\u0440\u0435\u0434\u0441\u0442\u0432\u0430\u043c\u0438 Python \u0447\u0435\u0440\u0435\u0437 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0443 saw-client \u0432&nbsp;<a href=\"https:\/\/pypi.org\/\">PyPI<\/a>. \u0420\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e Python \u043d\u0435&nbsp;\u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043b\u043e\u0436\u043d\u043e\u0441\u0442\u0438&nbsp;\u2014 \u0443\u043f\u0440\u0430\u0432\u043b\u0435\u043d\u0438\u0435 SAW \u043e\u0441\u0443\u0449\u0435\u0441\u0442\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0447\u0435\u0440\u0435\u0437 JSON-RPC API, \u043a\u0430\u043a \u043f\u043e\u043a\u0430\u0437\u0430\u043d\u043e \u0432&nbsp;<a href=\"https:\/\/galois.com\/blog\/2020\/10\/demo-control-saw-from-any-language\/\">\u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0439 \u0441\u0442\u0430\u0442\u044c\u0435<\/a>. \u0411\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 saw-client \u043f\u043e\u0441\u0442\u043e\u044f\u043d\u043d\u043e \u0440\u0430\u0437\u0432\u0438\u0432\u0430\u043b\u0430\u0441\u044c, \u0438&nbsp;\u0442\u0435\u043f\u0435\u0440\u044c \u0432&nbsp;\u043d\u0435\u0439 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d \u0432\u044b\u0441\u043e\u043a\u043e\u0443\u0440\u043e\u0432\u043d\u0435\u0432\u044b\u0439 \u0438\u043d\u0442\u0435\u0440\u0444\u0435\u0439\u0441, \u043e\u0442\u0432\u0435\u0447\u0430\u044e\u0449\u0438\u0439 \u0437\u0430&nbsp;\u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u0439 RPC.<\/p>\n<p>\u041f\u043e\u043c\u0438\u043c\u043e Python, \u0432&nbsp;SAW \u0442\u0430\u043a\u0436\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0430\u043b\u044c\u0442\u0435\u0440\u043d\u0430\u0442\u0438\u0432\u043d\u044b\u0439 \u044f\u0437\u044b\u043a \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u0446\u0435\u043d\u0430\u0440\u0438\u0435\u0432, \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u044b\u0439 SAWScript. \u0425\u043e\u0442\u044f \u043d\u0430&nbsp;SAWScript \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e \u043f\u0438\u0441\u0430\u0442\u044c \u0442\u0435&nbsp;\u0436\u0435 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438, \u0447\u0442\u043e \u0438&nbsp;Python, \u044d\u0442\u043e\u0442&nbsp;\u044f\u0437\u044b\u043a&nbsp;\u043d\u0435&nbsp;\u043b\u0438\u0448\u0451\u043d \u043d\u0435\u0434\u043e\u0441\u0442\u0430\u0442\u043a\u043e\u0432. SAWScript&nbsp;\u2014 \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u0438\u0437\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u044f\u0437\u044b\u043a, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043e\u043d&nbsp;\u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u0441\u043b\u043e\u0436\u0435\u043d \u0434\u043b\u044f \u043f\u043e\u043d\u0438\u043c\u0430\u043d\u0438\u044f \u0442\u0435\u043c\u0438, \u043a\u0442\u043e \u0432\u043f\u0435\u0440\u0432\u044b\u0435 \u0431\u0435\u0440\u0451\u0442\u0441\u044f \u0437\u0430&nbsp;\u0438\u0437\u0443\u0447\u0435\u043d\u0438\u0435&nbsp;SAW. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0432&nbsp;SAWScript \u043f\u0440\u0430\u043a\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043f\u043e\u0434\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u044f \u0432\u043d\u0435\u0448\u043d\u0438\u0445 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a. \u0415\u0441\u043b\u0438 \u0432\u044b&nbsp;\u0437\u0430\u0445\u043e\u0442\u0438\u0442\u0435 \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u043d\u0430&nbsp;SAWScript \u0442\u043e, \u0447\u0435\u0433\u043e \u043d\u0435\u0442 \u0432&nbsp;\u0441\u0442\u0430\u043d\u0434\u0430\u0440\u0442\u043d\u043e\u0439 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435, \u0432\u0430\u043c \u043f\u0440\u0438\u0434\u0451\u0442\u0441\u044f \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u043d\u0443\u0436\u043d\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u0441\u0430\u043c\u043e\u0441\u0442\u043e\u044f\u0442\u0435\u043b\u044c\u043d\u043e.<\/p>\n<p>\u0421&nbsp;\u0434\u0440\u0443\u0433\u043e\u0439 \u0441\u0442\u043e\u0440\u043e\u043d\u044b, Python&nbsp;\u2014 \u0448\u0438\u0440\u043e\u043a\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u044f\u0437\u044b\u043a, \u0438\u0437\u043d\u0430\u0447\u0430\u043b\u044c\u043d\u043e \u0445\u043e\u0440\u043e\u0448\u043e \u0437\u043d\u0430\u043a\u043e\u043c\u044b\u0439 \u0433\u043e\u0440\u0430\u0437\u0434\u043e \u0431\u043e\u043b\u044c\u0448\u0435\u043c\u0443 \u0447\u0438\u0441\u043b\u0443 \u043b\u044e\u0434\u0435\u0439. \u0423&nbsp;Python \u0442\u0430\u043a\u0436\u0435 \u0438\u043c\u0435\u0435\u0442\u0441\u044f \u0431\u043e\u0433\u0430\u0442\u044b\u0439 \u043d\u0430\u0431\u043e\u0440 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a \u0438&nbsp;\u0432\u0441\u043f\u043e\u043c\u043e\u0433\u0430\u0442\u0435\u043b\u044c\u043d\u044b\u0445 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c, \u0434\u043e\u0441\u0442\u0443\u043f\u043d\u044b\u0445 \u0432&nbsp;\u043a\u0430\u0442\u0430\u043b\u043e\u0433\u0435 PyPI. \u0414\u0430\u0436\u0435 \u0435\u0441\u043b\u0438 Python \u043d\u0435&nbsp;\u0432\u0445\u043e\u0434\u0438\u0442 \u0432&nbsp;\u0447\u0438\u0441\u043b\u043e \u0432\u0430\u0448\u0438\u0445 \u043b\u044e\u0431\u0438\u043c\u044b\u0445 \u044f\u0437\u044b\u043a\u043e\u0432 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f, \u043c\u044b&nbsp;\u0432\u0441\u0451 \u0440\u0430\u0432\u043d\u043e \u0441\u043e\u0432\u0435\u0442\u0443\u0435\u043c \u043f\u043e\u043f\u0440\u043e\u0431\u043e\u0432\u0430\u0442\u044c saw-client. \u0415\u0441\u043b\u0438 \u043f\u043e\u0434 \u0440\u0443\u043a\u043e\u0439 \u043d\u0435&nbsp;\u043e\u043a\u0430\u0436\u0435\u0442\u0441\u044f \u043d\u0438\u0447\u0435\u0433\u043e \u0434\u0440\u0443\u0433\u043e\u0433\u043e, \u043a\u043e\u0434, \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u043d\u044b\u0439 \u0432&nbsp;saw-client, \u043c\u043e\u0436\u0435\u0442 \u043f\u043e\u0441\u043b\u0443\u0436\u0438\u0442\u044c \u0438\u0441\u0442\u043e\u0447\u043d\u0438\u043a\u043e\u043c \u0432\u0434\u043e\u0445\u043d\u043e\u0432\u0435\u043d\u0438\u044f \u0434\u043b\u044f \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u0430\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u043e\u0433\u043e \u043a\u043b\u0438\u0435\u043d\u0442\u0430 \u043d\u0430&nbsp;\u0434\u0440\u0443\u0433\u043e\u043c \u044f\u0437\u044b\u043a\u0435.<\/p>\n<h3>\u0411\u0430\u0437\u043e\u0432\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0432&nbsp;saw-client<\/h3>\n<p>\u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c, \u043a\u0430\u043a saw-client \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0439 \u0440\u0435\u0430\u043b\u044c\u043d\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u043d\u0430&nbsp;\u044f\u0437\u044b\u043a\u0435&nbsp;C. \u0414\u043b\u044f \u043f\u0440\u0438\u043c\u0435\u0440\u0430 \u0432\u043e\u0437\u044c\u043c\u0451\u043c <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\">libsignal-protocol-c<\/a>. \u042d\u0442\u0430 \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u043d\u043d\u044b\u0439 \u043d\u0430&nbsp;\u044f\u0437\u044b\u043a\u0435 C&nbsp;<a href=\"https:\/\/en.wikipedia.org\/wiki\/Signal_Protocol\">\u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b Signal<\/a>, \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0439 \u0434\u043b\u044f \u0448\u0438\u0444\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u043c\u0433\u043d\u043e\u0432\u0435\u043d\u043d\u044b\u0445 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u0439, \u0433\u043e\u043b\u043e\u0441\u043e\u0432\u044b\u0445 \u0438&nbsp;\u0432\u0438\u0434\u0435\u043e\u0437\u0432\u043e\u043d\u043a\u043e\u0432. \u042d\u0442\u043e\u0442 \u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b \u043f\u0440\u0438\u043c\u0435\u043d\u044f\u0435\u0442\u0441\u044f \u0432&nbsp;<a href=\"https:\/\/signal.org\/\">\u043f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u0438 Signal Messenger<\/a>, \u043f\u043e\u043b\u0443\u0447\u0438\u0432\u0448\u0435\u043c \u043d\u0430\u0437\u0432\u0430\u043d\u0438\u0435 \u043f\u043e&nbsp;\u043f\u0440\u043e\u0442\u043e\u043a\u043e\u043b\u0443, \u043d\u043e&nbsp;\u0442\u0430\u043a\u0436\u0435 \u043f\u043e\u0434\u0434\u0435\u0440\u0436\u0438\u0432\u0430\u0435\u0442\u0441\u044f \u0432&nbsp;\u0434\u0440\u0443\u0433\u0438\u0445 \u043f\u0440\u0438\u043b\u043e\u0436\u0435\u043d\u0438\u044f\u0445, \u0442\u0430\u043a\u0438\u0445 \u043a\u0430\u043a WhatsApp, Facebook Messenger \u0438&nbsp;Skype.<\/p>\n<blockquote>\n<p>\u041e\u0431\u0449\u0435\u0435 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u0435\u0439 SAW \u0441&nbsp;\u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 libsignal-protocol-c \u043f\u0440\u0438\u0432\u0435\u0434\u0435\u043d\u043e \u0432&nbsp;\u0440\u0430\u0437\u0434\u0435\u043b\u0435 &#171;\u041f\u043b\u0430\u043d\u044b&#187;.<\/p>\n<\/blockquote>\n<p>\u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0431\u0430\u0437\u043e\u0432\u0443\u044e \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0443 \u0434\u0430\u043d\u043d\u044b\u0445, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u0443\u044e \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u043e\u0439 libsignal-protocol-c, \u0430&nbsp;\u0438\u043c\u0435\u043d\u043d\u043e <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\/blob\/3a83a4f4ed2302ff6e68ab569c88793b50c22d28\/src\/signal_protocol_internal.h%23L18-L21\">signal_buffer<\/a>:<\/p>\n<pre><code class=\"cpp\">struct signal_buffer {     size_t len;     uint8_t data[]; };<\/code><\/pre>\n<p>signal_buffer \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0441\u043e\u0431\u043e\u0439 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0439 \u043c\u0430\u0441\u0441\u0438\u0432 (\u043c\u0430\u0441\u0441\u0438\u0432 \u0434\u0430\u043d\u043d\u044b\u0445) \u0441&nbsp;\u0434\u043b\u0438\u043d\u043e\u0439&nbsp;len. \u041f\u0440\u0438 \u043e\u0442\u043f\u0440\u0430\u0432\u043a\u0435 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e libsignal-protocol-c \u043e\u0441\u043d\u043e\u0432\u043d\u044b\u043c \u043a\u043e\u043c\u043f\u043e\u043d\u0435\u043d\u0442\u043e\u043c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f signal_buffer.<\/p>\n<p>\u0427\u0442\u043e\u0431\u044b \u0431\u044b\u0442\u044c \u0443\u0432\u0435\u0440\u0435\u043d\u043d\u044b\u043c, \u0447\u0442\u043e libsignal-protocol-c \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0442\u0430\u043a, \u043a\u0430\u043a \u0437\u0430\u044f\u0432\u043b\u0435\u043d\u043e, \u043d\u0443\u0436\u043d\u043e \u0443\u0431\u0435\u0434\u0438\u0442\u044c\u0441\u044f, \u0447\u0442\u043e \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 signal_buffer \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u043e\u0436\u0438\u0434\u0430\u0435\u043c\u043e\u043c\u0443. \u0411\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u0442 \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0435 \u0434\u0432\u0443\u0445 \u0431\u0443\u0444\u0435\u0440\u043e\u0432 signal_buffer \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <a href=\"https:\/\/github.com\/signalapp\/libsignal-protocol-c\/blob\/3a83a4f4ed2302ff6e68ab569c88793b50c22d28\/src\/signal_protocol.c%23L591-L603\">signal_constant_memcmp<\/a>:<\/p>\n<pre><code class=\"cpp\">int signal_constant_memcmp(const void *s1, const void *s2, size_t n) {     size_t i;     const unsigned char *c1 = (const unsigned char *) s1;     const unsigned char *c2 = (const unsigned char *) s2;     unsigned char result = 0;      for (i = 0; i &lt; n; i++) {         result |= c1[i] ^ c2[i];     }      return result; }<\/code><\/pre>\n<p>\u0418\u043d\u0442\u0443\u0438\u0442\u0438\u0432\u043d\u043e \u043f\u043e\u043d\u044f\u0442\u043d\u043e, \u0447\u0442\u043e \u0443\u0442\u0438\u043b\u0438\u0442\u0430 signal_constant_memcmp \u0434\u043e\u043b\u0436\u043d\u0430 \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c, \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u043e&nbsp;\u043b\u0438 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u0434\u0432\u0443\u0445 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432 signal_buffer. \u0415\u0441\u043b\u0438 \u043e\u043d\u0438 \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b, \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0432\u0435\u0440\u043d\u0451\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435&nbsp;0. \u0415\u0441\u043b\u0438 \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u043d\u0435&nbsp;\u0441\u043e\u0432\u043f\u0430\u0434\u0430\u0435\u0442, \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442\u0441\u044f \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u0443\u043a\u0430\u0437\u044b\u0432\u0430\u044e\u0449\u0435\u0435 \u043d\u0430&nbsp;\u0431\u0430\u0439\u0442\u044b, \u0432&nbsp;\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u044b \u043e\u0442\u043b\u0438\u0447\u0430\u044e\u0442\u0441\u044f.<\/p>\n<p>\u041f\u0440\u0438 \u044d\u0442\u043e\u043c \u043d\u0430&nbsp;\u043f\u0435\u0440\u0432\u044b\u0439 \u0432\u0437\u0433\u043b\u044f\u0434 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043d\u0435\u043e\u0447\u0435\u0432\u0438\u0434\u043d\u043e, \u0447\u0442\u043e \u043f\u0440\u0438 \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u0430\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0432\u0435\u0440\u043d\u0451\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435&nbsp;0. \u0423\u0447\u0438\u0442\u044b\u0432\u0430\u044f, \u0447\u0442\u043e \u043c\u0430\u043d\u0438\u043f\u0443\u043b\u044f\u0446\u0438\u0439 \u0441&nbsp;\u0431\u0438\u0442\u0430\u043c\u0438 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043c\u043d\u043e\u0433\u043e, \u0432\u043f\u043e\u043b\u043d\u0435 \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e, \u0447\u0442\u043e \u043a\u0442\u043e-\u0442\u043e \u043c\u043e\u0433 \u0434\u043e\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u043e\u0448\u0438\u0431\u043a\u0443 \u043f\u0440\u0438 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0438\u0438 \u043a\u043e\u0434\u0430, \u043c\u0430\u043d\u0438\u043f\u0443\u043b\u0438\u0440\u0443\u044e\u0449\u0435\u0433\u043e \u0431\u0438\u0442\u0430\u043c\u0438. \u041f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0442\u0430\u043a\u043e\u0433\u043e \u043a\u043e\u0434\u0430 \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u0442\u044c, \u0441\u0432\u0435\u0440\u0438\u0432 \u0435\u0433\u043e \u0441\u043e&nbsp;\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0435\u0439, \u0441\u043e\u0437\u0434\u0430\u043d\u043d\u043e\u0439 \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e saw-client. \u0422\u0430\u043a\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043c\u043e\u0436\u0435\u0442 \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u0442\u044c \u043f\u0440\u0438\u043c\u0435\u0440\u043d\u043e \u0442\u0430\u043a:<\/p>\n<pre><code class=\"python\">from saw_client.llvm import *  class ConstantMemcmpEqualSpec(Contract):     def specification(self) -&gt; None:         _1          self.execute_func(_2)          _3<\/code><\/pre>\n<p>\u041a\u043b\u0430\u0441\u0441 Contract \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u0442 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 SAW \u0441&nbsp;\u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u043c\u0435\u0442\u043e\u0434\u0430 specification. \u0427\u0442\u043e\u0431\u044b \u0441\u043e\u0437\u0434\u0430\u0442\u044c \u0441\u043e\u0431\u0441\u0442\u0432\u0435\u043d\u043d\u0443\u044e \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044e, \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0441\u043e\u0437\u0434\u0430\u0442\u044c \u043f\u043e\u0434\u043a\u043b\u0430\u0441\u0441 Contract \u0438&nbsp;\u043f\u0435\u0440\u0435\u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u043c\u0435\u0442\u043e\u0434 specification. \u041a\u0430\u0436\u0434\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0441\u043e\u0441\u0442\u043e\u0438\u0442 \u0438\u0437&nbsp;\u0442\u0440\u0451\u0445 \u0447\u0430\u0441\u0442\u0435\u0439:<\/p>\n<ul>\n<li>\n<p>\u041f\u0440\u0435\u0434\u0432\u0430\u0440\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u0443\u0441\u043b\u043e\u0432\u0438\u044f (_1), \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0449\u0438\u0435 \u0434\u043e\u043f\u0443\u0449\u0435\u043d\u0438\u044f, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u043f\u0435\u0440\u0435\u0434 \u0432\u044b\u0437\u043e\u0432\u043e\u043c \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438.<\/p>\n<\/li>\n<li>\n<p>\u0410\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u044b \u0434\u043b\u044f \u043f\u0435\u0440\u0435\u0434\u0430\u0447\u0438 \u0432&nbsp;\u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e (_2).<\/p>\n<\/li>\n<li>\n<p>\u041f\u043e\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u044f (_3), \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0449\u0438\u0435 \u0445\u0430\u0440\u0430\u043a\u0442\u0435\u0440 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u043f\u043e\u0441\u043b\u0435 \u0432\u044b\u0437\u043e\u0432\u0430 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u0443\u0435\u043c\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438.<\/p>\n<\/li>\n<\/ul>\n<p>\u0423\u0447\u0438\u0442\u044b\u0432\u0430\u044f \u0442\u0440\u0435\u0431\u043e\u0432\u0430\u043d\u0438\u044f \u043a&nbsp;\u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438, \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u043c, \u043a\u0430\u043a \u0443\u0442\u0438\u043b\u0438\u0442\u0430 signal_constant_memcmp \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442 \u0432 \u043f\u0440\u0435\u0434\u0435\u043b\u0430\u0445 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 SAW:<\/p>\n<pre><code class=\"python\">class ConstantMemcmpEqualSpec(Contract):     n: int      def __init__(self, n: int):         super().__init__()         self.n = n      def specification(self) -&gt; None:         s1  = self.fresh_var(array_ty(self.n, i8), \"s1\")         s1p = self.alloc(array_ty(self.n, i8), points_to = s1)         s2  = self.fresh_var(array_ty(self.n, i8), \"s2\")         s2p = self.alloc(array_ty(self.n, i8), points_to = s2)         self.precondition(cryptol(f\"{s1.name()} == {s2.name()}\"))          self.execute_func(s1p, s2p, cryptol(f\"{self.n} : [64]\"))          self.returns(cryptol(\"0 : [32]\"))<\/code><\/pre>\n<p>\u041f\u0440\u0435\u0434\u0432\u0430\u0440\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u043c\u0438 \u0443\u0441\u043b\u043e\u0432\u0438\u044f\u043c\u0438 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u043d\u0430\u043b\u0438\u0447\u0438\u0435 \u0434\u0432\u0443\u0445 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432 (s1p \u0438&nbsp;s2p), \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 s1 \u0438&nbsp;s2&nbsp;\u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u043e. \u0412&nbsp;\u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, \u043e\u0434\u0438\u043d\u0430\u043a\u043e\u0432\u043e\u0441\u0442\u044c \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0433\u043e \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u0435\u0442 \u0432\u044b\u0437\u043e\u0432 self.precondition(&#8230;). \u0410\u0440\u0433\u0443\u043c\u0435\u043d\u0442 self.precondition(&#8230;) \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u043d\u0430&nbsp;<a href=\"https:\/\/cryptol.net\/\">Cryptol<\/a>, \u043f\u0440\u0435\u0434\u043c\u0435\u0442\u043d\u043e-\u043e\u0440\u0438\u0435\u043d\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f (DSL), \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u043e\u043c \u0432&nbsp;\u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0438. \u041f\u0440\u0438\u0432\u0435\u0434\u0451\u043d\u043d\u043e\u0435 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0435 \u043d\u0430&nbsp;Cryptol \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043f\u0440\u043e\u0441\u0442\u043e\u0435, \u0442\u0430\u043a \u043a\u0430\u043a \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442 \u0442\u043e\u043b\u044c\u043a\u043e \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0443 \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430, \u043d\u043e&nbsp;\u043d\u0438\u0436\u0435 \u043c\u044b&nbsp;\u0443\u0432\u0438\u0434\u0438\u043c \u0431\u043e\u043b\u0435\u0435 \u0441\u043b\u043e\u0436\u043d\u044b\u0435 \u043f\u0440\u0438\u043c\u0435\u0440\u044b \u043d\u0430&nbsp;Cryptol.<\/p>\n<p>\u0410\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430\u043c\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u044f\u0432\u043b\u044f\u044e\u0442\u0441\u044f \u0434\u0432\u0430 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u0430 \u0441&nbsp;\u0443\u043a\u0430\u0437\u0430\u043d\u0438\u0435\u043c \u0438\u0445&nbsp;\u0434\u043b\u0438\u043d (self.n), \u043f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u0443\u0435\u043c\u044b\u0445 \u0432\u043d\u0430\u0447\u0430\u043b\u0435 \u0432&nbsp;\u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0435 Cryptol, \u0447\u0442\u043e\u0431\u044b SAW \u043c\u043e\u0433 \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u043e&nbsp;\u043d\u0438\u0445 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435. \u041f\u043e\u0440\u0441\u0442\u0443\u0441\u043b\u043e\u0432\u0438\u0435, \u0441\u043d\u043e\u0432\u0430 \u0432&nbsp;\u0432\u0438\u0434\u0435 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f \u043d\u0430&nbsp;Cryptol, \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432&nbsp;\u0442\u043e\u043c, \u0447\u0442\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 0.<\/p>\n<p>\u041f\u043e\u0441\u043b\u0435 \u043f\u0440\u043e\u0432\u0435\u0434\u0435\u043d\u0438\u044f \u0432\u0441\u0435\u0439 \u043f\u043e\u0434\u0433\u043e\u0442\u043e\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e\u0439 \u0440\u0430\u0431\u043e\u0442\u044b \u043f\u0440\u043e\u0432\u0435\u0440\u044f\u0435\u043c, \u0447\u0442\u043e signal_constant_memcmp \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0443\u0435\u0442 \u0441\u043e\u0437\u0434\u0430\u043d\u043d\u043e\u0439 \u043d\u0430\u043c\u0438 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438:<\/p>\n<pre><code class=\"python\">mod = llvm_load_module(\"libsignal-protocol-c.bc\") # An LLVM bitcode file array_len = 42 # Pick whichever length you want to check llvm_verify(mod, \"signal_constant_memcmp\",  ConstantMemcmpEqualSpec(array_len))<\/code><\/pre>\n<p>\u0415\u0441\u043b\u0438 \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0430 \u043f\u0440\u043e\u0439\u0434\u0451\u0442 \u043d\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e, \u043c\u043e\u0436\u043d\u043e \u0437\u0430\u043f\u0443\u0441\u0442\u0438\u0442\u044c \u044d\u0442\u043e\u0442 \u043a\u043e\u0434 \u043d\u0430&nbsp;Python \u0438&nbsp;\u0443\u0432\u0438\u0434\u0435\u0442\u044c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442:<\/p>\n<pre><code>Verified: lemma_ConstantMemcmpEqualSpec (defined at signal_protocol.py:122)<\/code><\/pre>\n<p>\u0423\u0440\u0430! \u0418\u043d\u0441\u0442\u0440\u0443\u043c\u0435\u043d\u0442 SAW \u043f\u0440\u043e\u0432\u0435\u0440\u0438\u043b \u043f\u0440\u0430\u0432\u0438\u043b\u044c\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0431\u043e\u0442\u044b \u0443\u0442\u0438\u043b\u0438\u0442\u044b signal_constant_memcmp. \u0412\u0430\u0436\u043d\u043e \u043e\u0442\u043c\u0435\u0442\u0438\u0442\u044c, \u0447\u0442\u043e \u043d\u0430\u043c \u043d\u0435&nbsp;\u043d\u0443\u0436\u043d\u043e \u0431\u044b\u043b\u043e \u0434\u0430\u0436\u0435 \u0443\u043f\u043e\u043c\u0438\u043d\u0430\u0442\u044c \u043e&nbsp;\u0431\u0438\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u043d\u0438\u043f\u0443\u043b\u044f\u0446\u0438\u044f\u0445 \u0432\u043d\u0443\u0442\u0440\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u0438&nbsp;\u2014 SAW \u0432\u044b\u043f\u043e\u043b\u043d\u0438\u043b \u0438\u0445&nbsp;\u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438. \u041e\u0442\u043c\u0435\u0442\u0438\u043c, \u043e\u0434\u043d\u0430\u043a\u043e, \u0447\u0442\u043e \u043a\u043e\u043c\u0430\u043d\u0434\u0430 ConstantMemcmpEqualSpec \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u0442 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u044f\u0449\u0435\u0435 \u0442\u043e\u043b\u044c\u043a\u043e \u0432&nbsp;\u0442\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435, \u0435\u0441\u043b\u0438 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0435 \u043c\u0430\u0441\u0441\u0438\u0432\u044b \u0440\u0430\u0432\u043d\u044b \u0434\u0440\u0443\u0433 \u0434\u0440\u0443\u0433\u0443. \u0415\u0441\u043b\u0438&nbsp;\u0431\u044b \u043c\u044b&nbsp;\u0445\u043e\u0442\u0435\u043b\u0438 \u043e\u0445\u0430\u0440\u0430\u043a\u0442\u0435\u0440\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u044f\u0449\u0435\u0435 \u0432&nbsp;\u0441\u043b\u0443\u0447\u0430\u0435 \u043d\u0435\u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0430 \u0431\u0430\u0439\u0442\u043e\u0432\u044b\u0445 \u043c\u0430\u0441\u0441\u0438\u0432\u043e\u0432, \u043f\u043e\u0442\u0440\u0435\u0431\u043e\u0432\u0430\u043b\u0430\u0441\u044c&nbsp;\u0431\u044b \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0431\u043e\u043b\u0435\u0435 \u0441\u043b\u043e\u0436\u043d\u0430\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f.<\/p>\n<p>\u0422\u0430\u043a\u0436\u0435 \u0441\u043b\u0435\u0434\u0443\u0435\u0442 \u043e\u0442\u043c\u0435\u0442\u0438\u0442\u044c, \u0447\u0442\u043e \u0432&nbsp;\u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d\u043d\u043e\u043c \u0432\u044b\u0448\u0435 \u043a\u043e\u0434\u0435 \u0432\u0441\u0442\u0440\u0435\u0447\u0430\u044e\u0442\u0441\u044f \u043f\u043e\u0432\u0442\u043e\u0440\u0435\u043d\u0438\u044f, \u0442\u0430\u043a \u043a\u0430\u043a \u043c\u044b&nbsp;\u0434\u0432\u0430\u0436\u0434\u044b \u0432\u044b\u0437\u044b\u0432\u0430\u0435\u043c \u0444\u0443\u043d\u043a\u0446\u0438\u044e self.fresh_var(), \u0430&nbsp;\u0437\u0430\u0442\u0435\u043c self.alloc(). \u041a&nbsp;\u0441\u0447\u0430\u0441\u0442\u044c\u044e, Python \u0438\u0437\u0431\u0430\u0432\u043b\u044f\u0435\u0442 \u043e\u0442&nbsp;\u0442\u0430\u043a\u0438\u0445 \u043f\u0440\u043e\u0431\u043b\u0435\u043c:<\/p>\n<pre><code class=\"python\">def ptr_to_fresh(spec: Contract, ty: LLVMType,                  name: str) -&gt; Tuple[FreshVar, SetupVal]:     var = spec.fresh_var(ty, name)     ptr = spec.alloc(ty, points_to = var)     return (var, ptr)  class ConstantMemcmpEqualSpec(Contract):     ...      def specification(self) -&gt; None:         (s1, s1p) = ptr_to_fresh(self, array_ty(self.n, i8), \"s1\")         (s2, s2p) = ptr_to_fresh(self, array_ty(self.n, i8), \"s2\")         ...<\/code><\/pre>\n<h3>\u0412\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u043a\u043e\u0434\u0430 \u0441&nbsp;\u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c HMAC<\/h3>\n<p>\u041e\u0442&nbsp;\u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 libsignal-protocol-c \u0442\u0440\u0435\u0431\u0443\u0435\u0442\u0441\u044f \u0433\u043e\u0440\u0430\u0437\u0434\u043e \u0431\u043e\u043b\u044c\u0448\u0435, \u0447\u0435\u043c \u043f\u0440\u043e\u0441\u0442\u043e \u0445\u0440\u0430\u043d\u0438\u0442\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f&nbsp;\u2014 \u043e\u043d\u0430 \u0442\u0430\u043a\u0436\u0435 \u0434\u043e\u043b\u0436\u043d\u0430 \u043e\u0442\u043f\u0440\u0430\u0432\u043b\u044f\u0442\u044c \u0438&nbsp;\u043f\u043e\u043b\u0443\u0447\u0430\u0442\u044c&nbsp;\u0438\u0445. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0448\u0438\u0444\u0440\u043e\u0432\u0430\u0442\u044c \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0442\u0430\u043a, \u0447\u0442\u043e\u0431\u044b \u0438\u0445&nbsp;\u043c\u043e\u0433 \u043f\u0440\u043e\u0447\u0438\u0442\u0430\u0442\u044c \u0442\u043e\u043b\u044c\u043a\u043e \u043f\u0440\u0435\u0434\u043f\u043e\u043b\u0430\u0433\u0430\u0435\u043c\u044b\u0439 \u043f\u043e\u043b\u0443\u0447\u0430\u0442\u0435\u043b\u044c, \u0447\u0442\u043e\u0431\u044b \u0447\u0430\u0441\u0442\u043d\u0443\u044e \u043f\u0435\u0440\u0435\u043f\u0438\u0441\u043a\u0443 \u043d\u0435&nbsp;\u043c\u043e\u0433\u043b\u0438 \u043f\u0435\u0440\u0435\u0445\u0432\u0430\u0442\u0438\u0442\u044c \u0442\u0440\u0435\u0442\u044c\u0438 \u043b\u0438\u0446\u0430.<\/p>\n<p>\u041e\u0434\u043d\u0438\u043c \u0438\u0437&nbsp;\u043e\u0441\u043d\u043e\u0432\u043d\u044b\u0445 \u044d\u0442\u0430\u043f\u043e\u0432 \u0448\u0438\u0444\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u043f\u0440\u0438\u0441\u043e\u0435\u0434\u0438\u043d\u0435\u043d\u0438\u0435 <em>\u043a\u043e\u0434\u0430 \u0430\u0443\u0442\u0435\u043d\u0442\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f<\/em> (MAC), \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0434\u043b\u044f \u043f\u0440\u043e\u0432\u0435\u0440\u043a\u0438 \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u043f\u043e\u0441\u043b\u0435 \u043e\u0442\u043f\u0440\u0430\u0432\u043a\u0438 \u0441\u043e\u043e\u0431\u0449\u0435\u043d\u0438\u044f \u0435\u0433\u043e \u0441\u043e\u0434\u0435\u0440\u0436\u0438\u043c\u043e\u0435 \u043d\u0435&nbsp;\u043c\u0435\u043d\u044f\u043b\u043e\u0441\u044c. \u0412&nbsp;\u0447\u0430\u0441\u0442\u043d\u043e\u0441\u0442\u0438, libsignal-protocol-c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442 <a href=\"https:\/\/en.wikipedia.org\/wiki\/HMAC\">HMAC<\/a>, \u0442\u0438\u043f MAC, \u0432\u044b\u0447\u0438\u0441\u043b\u044f\u0435\u043c\u044b\u0439 \u0441&nbsp;\u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0445\u0435\u0448-\u0444\u0443\u043d\u043a\u0446\u0438\u0438.<\/p>\n<p>\u041f\u043e\u0434\u0440\u043e\u0431\u043d\u043e\u0435 \u043e\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u0440\u0430\u0431\u043e\u0442\u044b HMAC&nbsp;\u2014 \u0442\u0435\u043c\u0430 \u0434\u043b\u044f \u043e\u0442\u0434\u0435\u043b\u044c\u043d\u043e\u0439 \u0441\u0442\u0430\u0442\u044c\u0438. \u041d\u043e, \u043a&nbsp;\u0441\u0447\u0430\u0441\u0442\u044c\u044e, \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 SAW, \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u043e\u0439 \u0441&nbsp;HMAC, \u043d\u0435&nbsp;\u043d\u0443\u0436\u043d\u043e \u0432\u0434\u0430\u0432\u0430\u0442\u044c\u0441\u044f \u0432&nbsp;\u0434\u0435\u0442\u0430\u043b\u0438. \u0412\u043c\u0435\u0441\u0442\u043e \u044d\u0442\u043e\u0433\u043e \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c <em>\u043d\u0435\u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0438\u0440\u0443\u0435\u043c\u044b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438<\/em>. \u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u0441\u043e\u0437\u0434\u0430\u0434\u0438\u043c \u0440\u044f\u0434 \u0444\u0443\u043d\u043a\u0446\u0438\u0439 Cryptol, \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0449\u0438\u0445 \u0445\u0430\u0440\u0430\u043a\u0442\u0435\u0440 \u0440\u0430\u0431\u043e\u0442\u044b HMAC:<\/p>\n<pre><code class=\"haskell\">hmac_init : {n} [n][8] -&gt; HMACContext hmac_init = undefined  hmac_update : {n} [n][8] -&gt; HMACContext -&gt; HMACContext hmac_update = undefined  hmac_final : HMACContext -&gt; [SIGNAL_MESSAGE_MAC_LENGTH][8] hmac_final = undefined<\/code><\/pre>\n<p>\u042d\u0442\u043e \u0431\u0443\u0434\u0443\u0442 \u043d\u0435\u0438\u043d\u0442\u0435\u0440\u043f\u0440\u0435\u0442\u0438\u0440\u0443\u0435\u043c\u044b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0435 \u0434\u043b\u044f \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u043a\u043e\u0434\u0430, \u0441\u0432\u044f\u0437\u0430\u043d\u043d\u043e\u0433\u043e \u0441&nbsp;HMAC, \u0432&nbsp;\u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0435 libsignal-protocol-c. \u041e\u0441\u043d\u043e\u0432\u043d\u0430\u044f \u0438\u0434\u0435\u044f \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432&nbsp;\u0442\u043e\u043c, \u0447\u0442\u043e, \u043f\u043e\u043b\u0443\u0447\u0438\u0432 \u043d\u0430&nbsp;\u0432\u0445\u043e\u0434\u0435 \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0439 \u043a\u043b\u044e\u0447, hmac_init \u0441\u043e\u0437\u0434\u0430\u0441\u0442 HMACContext. HMACContext \u0431\u0443\u0434\u0435\u0442 \u043c\u043d\u043e\u0433\u043e\u043a\u0440\u0430\u0442\u043d\u043e \u043e\u0431\u043d\u043e\u0432\u043b\u044f\u0442\u044c\u0441\u044f \u0447\u0435\u0440\u0435\u0437 hmac_update, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u0434\u0430\u043d\u043d\u044b\u0435 \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430. \u0417\u0430\u0442\u0435\u043c hmac_final \u043f\u0440\u0435\u043e\u0431\u0440\u0430\u0437\u0443\u0435\u0442 HMACContext \u0432&nbsp;signal_buffer \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e\u0439 \u0434\u043b\u0438\u043d\u044b \u0434\u043b\u044f \u0445\u0440\u0430\u043d\u0435\u043d\u0438\u044f MAC.<\/p>\n<p>\u041e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 HMACContext \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442&nbsp;\u0442\u043e\u0433\u043e, \u043a\u0430\u043a\u0430\u044f \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0430\u044f \u0445\u044d\u0448-\u0444\u0443\u043d\u043a\u0446\u0438\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0432&nbsp;\u0441\u043e\u0447\u0435\u0442\u0430\u043d\u0438\u0438 \u0441&nbsp;HMAC. \u041f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u044b \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 libsignal-protocol-c \u043d\u0430\u0441\u0442\u0440\u043e\u0435\u043d\u044b \u0434\u043b\u044f \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c\u044b\u0445 \u0435\u044e&nbsp;\u0445\u0435\u0448-\u0444\u0443\u043d\u043a\u0446\u0438\u0439, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043c\u043e\u0436\u043d\u043e \u0441\u0432\u043e\u0431\u043e\u0434\u043d\u043e \u043f\u043e\u0434\u043a\u043b\u044e\u0447\u0430\u0442\u044c \u0431\u0438\u0431\u043b\u0438\u043e\u0442\u0435\u043a\u0438 <a href=\"https:\/\/www.openssl.org\/\">Op<\/a><\/p>\n<\/hr>\n<\/div>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-324553","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/324553","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=324553"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/324553\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=324553"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=324553"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=324553"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}