The OpenNET Project / Index page

[ новости /+++ | форум | теги | ]

форумы
правила/FAQ
поиск
регистрация
вход
слежка
RSS


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

Оглавление

Первый бета-выпуск Arti, реализации Tor на языке Rust, opennews (??), 02-Мрт-22, (0) [смотреть все]

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


85. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (71), 02-Мрт-22, 17:23 
Нет бы на KreMLin https://github.com/FStarLang/kremlin
Ответить | Правка | К родителю #1 | Наверх | Cообщить модератору

122. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (122), 02-Мрт-22, 22:48 
C таким названием на гитхабе можно уже и бан поймать
Ответить | Правка | Наверх | Cообщить модератору

128. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от InuYasha (??), 02-Мрт-22, 23:51 
но проект на самом деле прикольный )
Ответить | Правка | Наверх | Cообщить модератору

131. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (71), 03-Мрт-22, 06:12 
> прикольный

Заметь, ни одного абзаца обещаний безопасности.

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

139. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (-), 03-Мрт-22, 12:34 
>> HACL*, our High Assurance Crypto Library, provides numerous cryptographic primitives written in F*; these primitives enjoy memory safety,

...
>> By virtue of typing, any Low* program is memory safe.
>> ... a shallow embedding of a small, sequential, well-behaved subset of C in F*
>> ... provides the control required for writing efficient low-level security-critical code.
> Заметь, ни одного абзаца обещаний безопасности.

Продолжаешь газифицировать лужи?

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

140. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (71), 03-Мрт-22, 13:10 
> HACL*

Это частное мнение создателей библиотеки.

>  By virtue of typing, any Low* program is memory safe

Тоже частное мнение (анотация) к работе.

Будут цитаты из официальных страниц языка? Или опять гулко треснул?

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

141. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (-), 03-Мрт-22, 13:38 
>> We have written 20,000 lines of low-level F* code, implementing the TLS 1.3 record layer.
>> HACL*, our High Assurance Crypto Library,
>> (1) We provide HACL∗, a “high-assurance crypto library” implementing and proving

lines of Low∗) several cryptographic algorithms, including the Poly1305 MAC [Bernstein
> Это частное мнение создателей библиотеки.

Это повторный пук в лужу, под видом джакузи.

>> the ICFP 2017 Paper provides an overview of KreMLin as well as a paper formalization of our compilation toolchain
>> We illustrate the design of Low∗ using several examples from our codebase. We show the

ChaCha20 stream cipher [Nir and Langley 2015], focusing on memory safety (§2.1), and the
Poly1305 MAC [Bernstein 2005], focusing on functional correctness. (§2.3). Going beyond functional
> Тоже частное мнение (анотация) к работе.
> Будут цитаты из официальных страниц языка? Или опять гулко треснул?

Зачем ты продолжаешь газифицировать лужи?


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

142. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (71), 03-Мрт-22, 13:46 
> HACL∗

Эта библиотека - часть языка? Примитивы библиотеки обещают или язык?

> We
> our

Это язык или люди заявляют в своей (частной) работе?

> Зачем

так гулко?

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

144. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (-), 03-Мрт-22, 14:14 
>> HACL∗ <библиотека-демка от самих кремлинцев>
>> written in F*; these primitives enjoy memory safety
> Эта библиотека - часть языка? Примитивы библиотеки обещают или язык?

Твой юлеж и балабольство унылы.

>> We
>> our
> Это язык или люди заявляют в своей (частной) работе?

Завязывай уже с унылой демагоги^W попукиванием и передергом - язык не может что-то "заявлять", а "эти люди" и есть разработчики F*
https://www.fstar-lang.org/#people
ну и выставить "частной" работой ты пытаешься  
"Verified Low-Level Programming Embedded in F*"  
> We present Low∗, a language for low-level programming and verification, optimized cryptographic libraries. Low∗ is a shallow embedding of a smal
> ... By virtue of typing, any Low∗ program is memory safe. In addition, the programmer "

от них же.

>> Зачем
> так гулко?

Очередной унылус балаболус вульгарис сломался, вносите следующего.

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

145. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  –1 +/–
Сообщение от Аноним (71), 03-Мрт-22, 14:38 
>> Это язык или люди заявляют в своей (частной) работе?
> Завязывай уже с унылой демагоги^W

Согласен. Так язык или люди, используя речевые обороты с "we", "our", "by virtue of typing"?

Или безапелляционно, как раст, как язык гарантирует компилятором?

И заметь, эти заявления на сторонних сайтах.

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

146. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (-), 03-Мрт-22, 14:58 
>> Завязывай уже с унылой демагоги^W
> Согласен. Так язык или люди, используя речевые обороты с "we", "our", "by
> virtue of typing"?

И зачем ты продолжаешь, раз "согласен"?

> Или безапелляционно, как раст, как язык гарантирует компилятором?
> И заметь, эти заявления на сторонних сайтах.

https://www.fstar-lang.org/#introduction
>> You can learn more about F* by following the online tutorial and reading our papers.

https://www.fstar-lang.org/tutorial/
>> Given the implementation of a procedure, F* actually builds a mathematical proof that it is safe and correct with respect to its signature.

И заметь, даже усиленный юлеж^W демагогия тебе не помогли.

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

147. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  –1 +/–
Сообщение от Аноним (71), 03-Мрт-22, 15:21 
> https://www.fstar-lang.org
> https://www.fstar-lang.org/tutorial/

Это страница какого языка?

> Given the implementation of a procedure, F* actually builds a mathematical proof that it is safe and correct with respect to its signature.

И даже здесь где обещания безопасности _памяти_. Говорится про корректность согласно описанию. Описать можно и опасное поведение, в том числе порчу памяти.

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

148. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (-), 03-Мрт-22, 15:34 
>>>>> https://github.com/FStarLang/kremlin
>>>>> KreMLin is a tool that extracts an F* program
>>>>> ... Low*, a subset of F* ...
>> https://www.fstar-lang.org
>> https://www.fstar-lang.org/tutorial/
> Это страница какого языка?

"Папа, где море?"

> Аноним (71) Заметь, ни одного абзаца обещаний безопасности.
>>> any Low∗ program is memory safe.
> Аноним (71) <Нищитаица!>
>>> F* actually builds a mathematical proof that it is safe and correct
> Аноним (71) И даже здесь где обещания безопасности _памяти_. Говорится про корректность согласно описанию.

Опять унылый юлеж и переобувание в прыжке.


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

149. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  –1 +/–
Сообщение от Аноним (71), 03-Мрт-22, 15:49 
>>>>>> ... Low*, a subset of F* ...

Это один и тот же язык?

>>>>> KreMLin is a tool that extracts an F* program

Вот именно, этот инструмент может вытащить только то, что может вытащить, из более общего/мощного языка. При этом KreMLin даже из подмножества (Low*) не всё вытаскивает.

>>> any Low∗ program is memory safe.
>>> F* actually builds a mathematical proof that it is safe and correct

Бессистемная художественная аппликация из цитат.

Ты не понимаешь разницы между F*, Low* и KreMLin, и библиотек в составе других проектов. Дергаешь цитаты из разных языков. И даже там, все эти "безопасности" сказаны с использованием речевых оборотов "в силу сказанного".

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

151. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (-), 03-Мрт-22, 16:43 
>>> We present Low∗, a language for low-level programming and verification, optimized cryptographic libraries. Low∗ is a shallow embedding of a smal
>>> ... By virtue of typing, any Low∗ program is memory safe. In addition, the programmer "
> Это один и тот же язык?

Память как у рыбки?

> Бессистемная художественная аппликация из цитат.
> Ты не понимаешь разницы между F*, Low* и KreMLin, и библиотек в
> составе других проектов. Дергаешь цитаты из разных языков. И даже там,
> все эти "безопасности" сказаны с использованием речевых оборотов "в силу сказанного".

Юли Балаб^W Емеля, твоя неделя.

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

152. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  –1 +/–
Сообщение от Аноним (71), 03-Мрт-22, 17:12 
>>> By virtue of typing...

Цитата из стороннего сайта про Low*. Еще раз повторить "Память как у рыбки?"

> Балаб^W

Если что, то компилятор F* компилирует/транслирует в ocaml, который с менеджером памяти и GC. Причем тут "безопасность памяти"?

Low* это подмножество F*, для которого можно написать компилятор/транслятор на Си (без использования менеджера памяти и gc).

HACL* - это библиотека из другого проекта с _примитивами_, которые "что-то там гарантируют".

KreMLin (про который весь сыр-бор) не полностью поддерживает Low*, не может транслировать в человеко-читаемый Си-код.

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

153. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (-), 03-Мрт-22, 18:09 
>>>> By virtue of typing...
> Цитата из стороннего сайта про Low*. Еще раз повторить "Память как у рыбки?"

Рыбка, пересмотри еще раз сайт и авторов.
Цитата из работы, представленняющей KreMLin-Low на ICFP (International Conference on Functional Programming), на которую ссылаются с гитхабостраницы проекта
>>> This work has been formalized on paper. We state that the compilation of such F* programs to C preserves semantics. We start from Low*, a subset of F*, and relate its semantics to CompCert's Clight.
>>> the ICFP 2017 Paper [ссылка] provides an overview of KreMLin as well as a paper formalization of our compilation toolchain"

и в которой (работе) в списке авторов без особого труда можно увидеть самых активных коммитеров
https://github.com/FStarLang/kremlin/graphs/contributors

...
> прочий унылый юлеж поскипан
>

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

154. "Первый бета-выпуск Arti, реализации Tor на языке Rust"  +/–
Сообщение от Аноним (71), 03-Мрт-22, 18:49 
Ты еще путаешь людей, (одних и тех же) участвующих в разных проектах, которые высказываются применительно к проекту. И то, что  написано про проект hacl*, применяешь к kremlin, и то что написано про F*.

Привет, аноним с проблемами с абстракциями!

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

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

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




Партнёры:
PostgresPro
Inferno Solutions
Hosting by Hoster.ru
Хостинг:

Закладки на сайте
Проследить за страницей 		Created 1996-2024 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру