https://www.opennet.ru/openforum/vsluhforumID3/139772.html Несколько выявленных за последние дни опасных уязвимостей, большинство из которых можно эксплуатировать удалённо:...<br><br>Подробнее: https://www.opennet.ru/opennews/art.shtml?num=65183<br> https://www.opennet.ru/openforum/vsluhforumID3/139772.html#78 Fri, 10 Apr 2026 18:04:35 GMT &gt; тут уже спеку на анализ давать надо, а не код (имплементацию) <br><br>ЕМНИП они заверяли, что там верифицирована работа с памятью. Почему бы не попробовать найти вулны в генерированном си коде?<br> https://www.opennet.ru/openforum/vsluhforumID3/139772.html#77 Fri, 10 Apr 2026 17:56:49 GMT &gt;&gt; Ну дак это искусственные условия. На практике многие утверждения приходится аксиоматизировать. Что-то остается недоказанным. Что-то приходится допускать.<br>&gt; Это как раз не исукственные условия - это условия, которые ты контролируешь <br>&gt; на уровне алгоритма. Все поведение за пределами алгоритма (например, сломанное железо) <br>&gt; к самому алгоритму и его реализации в коде отношения не имеет, <br>&gt; и, соответсвенно, чисто физически не сожет быть математически верифицируемым.<br>&gt; Это как бы очевидно, не?<br><br>Нет. Это выставление условий модели удобных для доказательства. В sel4 доказывают не про исходник, а про модель на haskell, доказывают не полные свойства, а некоторые урезанные варианты, в урезанных конфигурациях. <br> https://www.opennet.ru/openforum/vsluhforumID3/139772.html#76 Fri, 10 Apr 2026 17:56:43 GMT 1. все это описанно в книжке Пети Ж.-П. "О чем размышляют роботы?" советское издание 1987 год, оригинал 1982 год.<br><br>В книге известного французского ученого дается оригинальное изложение основных тенденций развития роботов с программным управлением, адаптацией и элементами искусственного интеллекта, построенное на многочисленных забавных иллюстрациях. Однако такая занимательность подачи материала не означает элементарности содержания.<br><br>2. Проблематика "современной" математики, широкой публике непонятна уже более тысячи лет.<br>и что?<br> https://www.opennet.ru/openforum/vsluhforumID3/139772.html#75 Fri, 10 Apr 2026 17:53:46 GMT &gt;[оверквотинг удален]<br>&gt; верификацию как за самообман, тоже самое можно сказать про всю математику, <br>&gt; где есть допущения, аксиомы и другие "неловкие" моменты, и все сведется <br>&gt; к тому, а что есть собственно понятие - "доказать" (формально доказать). <br>&gt; Брауэр вообще не признавал доказательства от противного :) <br>&gt; Вот seL4 описали эти моменты: <br>&gt; //sel4.systems/Verification/proofs.html <br>&gt; //sel4.systems/Verification/implications.html <br>&gt; //sel4.systems/Verification/assumptions.html <br>&gt; А вот тут про ironclad-os: <br>&gt; //ironclad-os.org/formalverification.html <br><br>Ответил здесь https://www.opennet.ru/openforum/vsluhforumID3/139772.html#74<br><br> https://www.opennet.ru/openforum/vsluhforumID3/139772.html#74 Fri, 10 Apr 2026 17:52:50 GMT &gt;&gt; Найди и покажи такую верификацию <br>&gt; Вот <br>&gt; //sel4.systems/Verification/proofs.html <br>&gt; //sel4.systems/Verification/implications.html <br>&gt; //sel4.systems/Verification/assumptions.html <br><br>А внутрь ты смотрел?<br><br>Доказывают они, на самом деле, свойства урезанной статичной версии ядра https://github.com/seL4/l4v/blob/59b2d2f630119be823f3f44465119b4fec7bc34a/spec/sep-abstract/README.md?plain=1#L10<br><br>&gt; This specification is a cut-down version of the seL4 abstract specification<br>&gt; that removes all system calls apart from notifications. The resulting kernel<br>&gt; is a classic static separation kernel without any dynamism.<br>&gt; <br>&gt; A proof that seL4 is equivalent to this cut-down version if configured<br>&gt; appropriately can be found in the `proof` directory under<br>&gt; [`bisim`](../../proof/bisim/).<br><br>Переходим https://github.com/seL4/l4v/tree/59b2d2f630119be823f3f44465119b4fec7bc34a/proof/bisim и читаем<br><br>&gt; This proof establishes that seL4, if configured fully statically with 1-level CSpaces and notification caps only, i https://www.opennet.ru/openforum/vsluhforumID3/139772.html#73 Fri, 10 Apr 2026 17:47:46 GMT На Си только илита пишет, они не ошибаются! 12yoexpert не даст соврать!<br> https://www.opennet.ru/openforum/vsluhforumID3/139772.html#72 Fri, 10 Apr 2026 17:42:56 GMT все в этом мире гораздо дырявее чем мы думаем!!!<br><br>весь мир -- дыра!!!)))<br> https://www.opennet.ru/openforum/vsluhforumID3/139772.html#71 Fri, 10 Apr 2026 17:37:36 GMT Никогда не будет. Появятся новые типы уязвимостей, и новые способы защиты от них. Война щита и меча. С ростом мощи искусственного интеллекта люди перестанут в своей массе понимать его выводы, но будут всё больше и больше слепо на него полагаться. Это уже происходит, но это лишь начало. Постепенно даже те, кто будут пытаться его понять, смогут иметь лишь набор возможных интерпретаций относительного того, что он мог бы иметь в виду. В новой форме воскреснут такие средневековые дисциплины, как герменевтика, экзегетика и схоластика, но уже применительно к его отровениям.<br> https://www.opennet.ru/openforum/vsluhforumID3/139772.html#70 Fri, 10 Apr 2026 17:16:22 GMT Это ещё даже Алису не попробовали<br>