forum.opennet.ru

Форум Разговоры, обсуждение новостей
Вариант для распечатки		Пред. тема \| След. тема
Режим отображения отдельной подветви беседы		[ Отслеживать ]

Оглавление

Результаты второго аудита безопасности разработок проекта Tor, opennews (??), 30-Янв-24, (0) [смотреть все]

Каковы методы аудита Фуззинг Не верится, что всё вручную , Аноним (4), 18:17 , 30-Янв-24, (4) //

Не похоже Какой фаззинг додумается до bridge_lines А zip-бомба это вообще пер, Карлос Сношайтилис (ok), 19:38 , 30-Янв-24, (43) //

В оригинале pdf по ссылке code audit и crystal box То есть код смотрели Скан, n00by (ok), 20:11 , 30-Янв-24, (56) +1 //

Может они без исходников за 50x в дисассемблере сидят и то же самое проверяют , Электрон (?), 07:06 , 31-Янв-24, (84)

В такое я не верю Лично у меня систематическая ошибка при переписывании с асма , n00by (ok), 16:48 , 31-Янв-24, (100)

Arti,я так понимаю, тестировать не стали Типа не готово ещё , anonymous (??), 19:05 , 30-Янв-24, (29) //

Нет аудита - нет и уязвимостей А то мог бы получится и конфуз с утратой доверия, Аноним (35), 19:19 , 30-Янв-24, (35) +2 //

О, вы прогрессируете Раньше было нет кода - нет уязвимостей , а теперь не ауд, Аноним (-), 19:57 , 30-Янв-24, (53) +4 //

Проблема раста в том, что его сложно читать, низкая популярность и дефицит специ, Аноним (57), 20:36 , 30-Янв-24, (57) –1

тем, кто на нем не писал, это даа все остальным норм, не сложнее чем крестыа мож, Аноним (-), 21:36 , 30-Янв-24, (63) +3

Лукавишь В плюсах нет такого количества закорючек и всё более наглядно, зачасту, Аноним (57), 21:44 , 30-Янв-24, (65)

Ну и самая частая, это постоянные падения по поводу и без Например, я пытался и, Аноним (57), 21:50 , 30-Янв-24, (66) –2
Хоть бы доку открыл https nnethercote github io perf-book profiling htmlсильно, Аноним (-), 21:55 , 30-Янв-24, (67) +3

Просто ты теоретик Я основываюсь на собственном опыте и отзывах жертв ржавчины , Аноним (57), 22:51 , 30-Янв-24, (74) –1

А, ну так начал бы с того, что ты хейтер, я бы не тратил время Неосияторы есть в, Аноним (-), 23:20 , 30-Янв-24, (75)

Я не хейтер, мне нравится раст рядом идей Пока асинхронных генераторов нет, о с, Аноним (57), 23:30 , 30-Янв-24, (76)

Так и пиши закорючки меня расстраивают, они заставляют напрягаться опилкам в мо, Аноним (-), 22:10 , 30-Янв-24, (69)

Каждый раз поражаюсь какое доброжелательное у Раста коммьюнити, и почему многие , Аноним (82), 02:59 , 31-Янв-24, (82) –1

По сравнению со злобными функциональщиками в свое время просто зайки , Ф1 (?), 09:08 , 31-Янв-24, (86)

С чего вдруг Они сами пишут что Аоти только дорос до версии 1 0 и там еще кучу , Аноним (-), 22:03 , 30-Янв-24, (68) +1 //

Не проекты на Rust, а проект только RustVMM И еще они провели аудит полсотни, Аноним (82), 02:46 , 31-Янв-24, (79)

ждут когда chatgpt протестирует за них, Аноним (39), 19:30 , 30-Янв-24, (39)

Для проекта, который разрабатывается на Си, нетипично мало ошибок Вероятно, это, Bottle (?), 19:33 , 30-Янв-24, (40) //

Это те люди, которые ещё аудит заказывают Респект, вне зависимости от языка, ибо, Карлос Сношайтилис (ok), 19:40 , 30-Янв-24, (44) +6 //

Эх, вот бы придумали такой, где отсутствие логических ошибок можно доказать, да , Аноним (61), 21:31 , 30-Янв-24, (61) //

Так есть же уже - формальная верификация и все дела Но на них настолько дорого , Аноним (-), 22:17 , 30-Янв-24, (70) +1

Сегодня есть спарк ада , отзывы говорят, что подорожание незначительно , Аноним (57), 22:32 , 30-Янв-24, (72)

GNATprove - инструмент для формальной верификации языка SPARK Он проверяет соот, Аноним (82), 02:51 , 31-Янв-24, (80)

Давно придумали и не один, из самых практичных это ATS https www cs bu edu hw, Ф1 (?), 09:06 , 31-Янв-24, (85)

Просто это не первый аудит Плюс там сильная команда, которая старается писать оч, Аноним (-), 19:59 , 30-Янв-24, (54) //

Хм, так выходит метод писать нормально и не допускать очевидной лажи все же ра, Аноним (82), 02:11 , 31-Янв-24, (78) +3 //

не забывай что эта же команда также применила метод переписать свой продукт на , Советский инженер (ok), 10:03 , 31-Янв-24, (88)

все могут ошибаться, никто не идеален, Аноним (89), 10:33 , 31-Янв-24, (89)

Не работает, потому что оно требует неоправданно много трудозатрат И все равно , Аноним (-), 10:38 , 31-Янв-24, (90)

Им просто финансирование нужно осваивать Иначе зачем им деньги давать, если все, Аноним (103), 19:02 , 01-Фев-24, (103)

Что ни говорите, а живые программисты -- слабое звено современного IT , Аноним (59), 21:05 , 30-Янв-24, (59) //

Смотри шире Живые люди - слабое звено современного мира , Аноним (60), 21:18 , 30-Янв-24, (60) +4 //

Скрыто модератором, Аноним (-), 11:32 , 31-Янв-24, (93)

Cовременного O_o Диды не могли правильно посчитать размер массива еще когда икс, Аноним (-), 22:50 , 30-Янв-24, (73) //

А мы еще посмотрим как потомки будут разбирать те залежи гуано, что сегодняшние , Аноним (82), 02:56 , 31-Янв-24, (81)

да ты в сервис сходи, аха, Аноним (77), 02:05 , 31-Янв-24, (77)
То что сейчас почему-то называют ИИ по надежности вообще ниже плинтуса , Ф1 (?), 09:12 , 31-Янв-24, (87)

То есть теперь официально запруфано, что Си-версия Тора более чем безопасна Это, Аноним (82), 03:03 , 31-Янв-24, (83) +1 //

Да, после кучи времени разработки, багов и аудитов они решили просто переписа, Аноним (-), 10:44 , 31-Янв-24, (91) //

То есть навсегда Фух, можно выдохнуть У напичканной закладками NSA версии на, Аноним (103), 18:58 , 01-Фев-24, (102)

Пацаны, что там с подозрительным товарищ-майоровским входным нодом Когда подклю, Аноним (-), 11:30 , 31-Янв-24, (92) +1 //

Ни хрена не разумеется Каждый экземпляр TOR-клиента имеет локальную актуальную , Аноним (60), 12:33 , 31-Янв-24, (94) //

А разве сам факт подключения к анонимной враждебной сети не будет уже флажком дл, Аноним (-), 12:43 , 31-Янв-24, (95) +1 //

Конечно является Потому что в мире есть отбитые, которое кричат, что https это з, Аноним (-), 12:56 , 31-Янв-24, (96)
В случае TOR вариантов нет Facebook, Twitter, Reddit, ProtonMail, DuckDuckGo, De, Аноним (60), 13:13 , 31-Янв-24, (97)

Хорошо Тогда вопрос Кто контроллирует сервер входной ноды во Франции Не ду, Аноним (-), 13:46 , 31-Янв-24, (98) //

В РФ провайдеры негласно РКН официально не запрещает TOR блокируют входные нод, Аноним (60), 14:00 , 31-Янв-24, (99)
И оплачивают его - DARPA- U S Department of State Bureau of Democracy, Human Ri, Аноним (60), 22:51 , 31-Янв-24, (101) +1

Сообщения [Сортировка по времени | RSS]

61. "Результаты второго аудита безопасности разработок проекта To..." +/–

Сообщение от Аноним (61), 30-Янв-24, 21:31

Эх, вот бы придумали такой, где отсутствие логических ошибок можно доказать, да? Хотя не, тогда не получится каждый год заказывать аудит за деньги спонсоров.

Ответить | Правка | Наверх | Cообщить модератору

70. "Результаты второго аудита безопасности разработок проекта To..." +1 +/–

Сообщение от Аноним (-), 30-Янв-24, 22:17

Так есть же уже - формальная верификация и все дела.
Но на них настолько дорого "писать", что дешевле каждый год аудиты заказывать. И так лет на 100 хватит.
PS. Почитайте на досуге, сколько лет и денег ушло на формальную верификацию ядра seL4, с его жалкими "8,700 lines of C code and 600 lines of assembler". Статья "seL4: Formal Verification of an OS Kernel" в открытом доступе на сайте Columbia University.

Ответить | Правка | Наверх | Cообщить модератору

72. "Результаты второго аудита безопасности разработок проекта To..." +/–

Сообщение от Аноним (57), 30-Янв-24, 22:32

Сегодня есть спарк (ада), отзывы говорят, что подорожание незначительно.

Ответить | Правка | Наверх | Cообщить модератору

80. "Результаты второго аудита безопасности разработок проекта To..." +/–

Сообщение от Аноним (82), 31-Янв-24, 02:51

GNATprove - инструмент для формальной верификации языка SPARK. Он проверяет соответствие подмножеству SPARK и выполняет анализ потока и доказательство исходного кода. Этот может потребовать дополнительного времени, но взамен предоставляет гарантии корректности кода. Если цель улучшение качества и надежности программного обеспечения, то оно того конечно же стоит.

Ответить | Правка | Наверх | Cообщить модератору

85. "Результаты второго аудита безопасности разработок проекта To..." +/–

Сообщение от Ф1 (?), 31-Янв-24, 09:06

>Эх, вот бы придумали такой, где отсутствие логических ошибок можно доказать, да?
Давно придумали и не один, из самых практичных это ATS https://www.cs.bu.edu/~hwxi/atslangweb/
Но закорючки раста просто глаза будут радовать, в сравнении с тем сколько лишнего нужно писать на подобных языках чтобы все было доказано.

Ответить | Правка | К родителю #61 | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема

Партнёры:

Хостинг:

Закладки на сайте
Проследить за страницей

Created 1996-2024 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру


	61. "Результаты второго аудита безопасности разработок проекта To..."	+/–
	Сообщение от Аноним (61), 30-Янв-24, 21:31
	Эх, вот бы придумали такой, где отсутствие логических ошибок можно доказать, да? Хотя не, тогда не получится каждый год заказывать аудит за деньги спонсоров.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	70. "Результаты второго аудита безопасности разработок проекта To..."	+1 +/–
	Сообщение от Аноним (-), 30-Янв-24, 22:17
	Так есть же уже - формальная верификация и все дела. Но на них настолько дорого "писать", что дешевле каждый год аудиты заказывать. И так лет на 100 хватит. PS. Почитайте на досуге, сколько лет и денег ушло на формальную верификацию ядра seL4, с его жалкими "8,700 lines of C code and 600 lines of assembler". Статья "seL4: Formal Verification of an OS Kernel" в открытом доступе на сайте Columbia University.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	72. "Результаты второго аудита безопасности разработок проекта To..."	+/–
	Сообщение от Аноним (57), 30-Янв-24, 22:32
	Сегодня есть спарк (ада), отзывы говорят, что подорожание незначительно.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	80. "Результаты второго аудита безопасности разработок проекта To..."	+/–
	Сообщение от Аноним (82), 31-Янв-24, 02:51
	GNATprove - инструмент для формальной верификации языка SPARK. Он проверяет соответствие подмножеству SPARK и выполняет анализ потока и доказательство исходного кода. Этот может потребовать дополнительного времени, но взамен предоставляет гарантии корректности кода. Если цель улучшение качества и надежности программного обеспечения, то оно того конечно же стоит.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	85. "Результаты второго аудита безопасности разработок проекта To..."	+/–
	Сообщение от Ф1 (?), 31-Янв-24, 09:06
	>Эх, вот бы придумали такой, где отсутствие логических ошибок можно доказать, да? Давно придумали и не один, из самых практичных это ATS https://www.cs.bu.edu/~hwxi/atslangweb/ Но закорючки раста просто глаза будут радовать, в сравнении с тем сколько лишнего нужно писать на подобных языках чтобы все было доказано.
	Ответить \| Правка \| К родителю #61 \| Наверх \| Cообщить модератору