Организация RISC-V Foundation сообщила о верификации работы микроядра seL4 на системах с архитектурой набора команд RISC-V. Верификация сводится к математическому доказательству надёжности работы seL4, которое свидетельствует о полном соответствии заданным на формальном языке спецификациям. Доказательство надёжности позволяет использовать seL4 в критически важных системах на базе процессоров RISC-V RV64, требующих повышенного уровня надёжности и гарантирующих отсутствие сбоев...Подробнее: https://www.opennet.me/opennews/art.shtml?num=53129
осталось только распространить risc-v в массах. и тогда можно будет закопать x86
Закопать то вряд ли, но это явно тот путь, по которому следует развиваться
Интел не позволит, закопают всех конкурентов в округе.
> Интел не позволит, закопают всех конкурентов в округе.Сначала интелю нужно повторить трюк Мюнхгаузена (вытащить себя за волосы), а уж потом может-быть, если повезет...
> Интел не позволит, закопают всех конкурентов в округе.Копать устанут - его уже толпа фирм взяли в оборот.
И кстати говорят что скоро фирму Интел будет ждать еще один приятный подарок: Эпл вроде бы на днях должен анонсировать переход на 64-битные ARM... :)
>осталось только распространить risc-v в массахТю, мелочи-то какие. Займёмся сразу после отказа от империализма и излечения всех болезней.
Жалеешь 140 рублей?
?
https://www.crowdsupply.com/sifive/hifive1-rev-b
Мне показывает $59.
https://aliexpress.ru/item/4000818117666.html?algo_pvid=39bb...,searchweb201602_,searchweb201603_
Трусы Большой Мужчина Женщина Купить Большой Проститутка Шланг
Просто любопытно: вы в самом деле пользуетесь сайтом aliexpress на русском языке?
Серьёзно? Это не шутка? Вот прямо так его и читаете — со всеми их шлангами и многими удовольствиями?
> Просто любопытно: вы в самом деле пользуетесь сайтом aliexpress на русском языке?
> Серьёзно? Это не шутка? Вот прямо так его и читаете — со
> всеми их шлангами и многими удовольствиями?Нисколько не поклонник, но разве на английском там сильно меньше "удовольствий"?
Удивительно, но всё-таки сильно меньше. По крайней мере, у меня такая выборка.
Английский более информативный.
А ты пользуешься китайским вариантом или просто думаешь, что для алика родной английский?
Алиэкспресс ориентируется на английский т.к. международный. Таобао мандаринский т.к. внутренний.
> А ты пользуешься китайским вариантом или просто думаешь, что для алика родной английский?Просто на английском покупает сильно больше - так что этим можно и нормальный перевод живыми переводчиками. А россиянам с их объемами рынка только на гуглтранслейт хватает. Поэтому русское описание товаров на али...
Насколько знаю, при заходе с IP-адресов из RU областей aliexpress крайне настойчиво перенаправляет на версию с этим хтоническим ужасом от мира машинного перевода. И отучить его от этого настройками сайта и даже плагинами браузера становится всё труднее и труднее. Это какое-то безумие.
На английский переключаю, мандаринским ещё не овладел чтобы таобао читать.
Но русскоязычный Ali показывает цены в национальной валюте. В которой мы и платим.
> Но русскоязычный Ali показывает цены в национальной валюте. В которой мы и платим.Понять по русскому описанию товара что это за неведомая штука в сколь-нибудь продвинутых случаях решительно невозможно. Но если хочется почитать анекдоты, пойдет.
Промт-онлайн с ангийской версии Али не сильно лучше переведёт.
> Промт-онлайн с ангийской версии Али не сильно лучше переведёт.А мне оно и не надо. Если бы я не умел в инглиш, мой потолок в IT ограничивался бы заменой плашки памяти в древнем компе жэка. Оно мне надо?
> Get a single HiFive1 Rev B dev kit, featuring the FE310-G002,
> SiFive's second generation open source RISC-V 32-bit SoC.Кому этот перемикроконтроллер нужен-то?
Их rv64gc за килобакс производительностью не радует, а это...
Производителям домашней автоматизации.
Домашним автоматизаторам хватит пригоршни ЛА3
> Домашним автоматизаторам хватит пригоршни ЛА3Да что там, спичек и желудей.
ЛА3 потребуется очень большая пригоршня, т.к. триггеры, счётчики, регистры тоже придётся на них делать. Отсюда, к тому же, большое энергопотребление. И самое главное - жёсткая логика, нет гибкости.
Как минимум, тем же, кому и остальные микроконтроллеры.GigaDevice вообще презанятная контора в плане Особого Пути™.
Впервые я на них наткнулся с их клонами STM32 (GD32Fxxx): pin-to-pin совместимые клоны с без всякого стеснения срисованными даташитами и периферией. И, как минимум, одной маааленькой фишкой: бóльший объём flash-ROM за ту же или даже меньшую цену, достигли они этого за счёт того что вместо полноценной параллельной дорогой флеш-памяти (как у оригинала от ST) использовали отдельный кристалл последовательной флеш-памяти, разварив и залив несколько кристаллов в одном корпусе. А чтобы это не угробило производительность, они добавили между флеш-памятью и ядром дополнительное ОЗУ для кеширования, в итоге в некоторых задач (когда горячая область кода влезает в этот кеш) этот клон работает быстрее оригинала (где либо терпи wait states при чтении/исполнении из флеша, либо ручками копируй горячие функции в основное ОЗУ, либо бери более дорогой камень с кешем из коробки).
Потом они же придумали такой прикол, как серию из почти полных аналогов чипов серии STM32F0 (которые на весьма урезанном Cortex-M0), но с одним важным отличием в виде полноценного ядра Cortex-M3 (как у STM32F1). Это давно напрашивалось, но ST это посчитали не очень-то нужным, а подвальные китайцы взяли и реализовали.
Здесь вот другой их не менее впечатливший выкрутас — придумать серию GD32V, где вся периферия (включая адреса для MMIO) взята от соответствующих STM32Fxxx, но ядро заменено на RISC-V, т.е. в работающем проекте достаточно заменить несколько мест из CMSIS (типа использования инструкции WFI, wait for interrupt) и пересобрать другим компилятором, чтобы получить максимально безболезненный переход с ARM на RISC-V.
Т.е. с одной стороны — бесстыднейшее (и крайне спорное с юридической точки зрения) копирование и паразитирование на чужих идеях и наработках, а с другой — придумали и внедрили нечто мелкое, но очень даже полезное (не для всех, конечно). Пардон за такой оффтоп, но надеюсь что кому-то это тоже окажется интересным ~открытием или дополнят/поправят (раз уж затронули такую интересную мне тему).
Спасибо! В отличие от 90% флуда на этом сайте - у вас очень интересное сообщение
> минимум, одной маааленькой фишкой: бóльший объём flash-ROM за ту же или даже меньшую ценуЕще у них есть ответвления F1xx-like которых в оригинале нет - например мелкие QFN с USB и общим видом железа как у F1xx. У STMicro именно такого комбо почему-то и нет, при всем разнообразии. Неужто никто usb не хотел в мелком корпусе c F1xx? Да ну ладно?!
> кристалл последовательной флеш-памяти, разварив и залив несколько кристаллов в одном корпусе.
А вы их щупали? Флеху шить программно пробовали? Оно по flash controller не совместимо? А то даташит вроде как клон STM-ов 1 в 1.
> Здесь вот другой их не менее впечатливший выкрутас — придумать серию GD32V,
> где вся периферия (включая адреса для MMIO) взята от соответствующих STM32Fxxx,
> но ядро заменено на RISC-V,Вот это они очень стебно прикололись. Надо будет как-нибудь повертеть в руках этот неведомый пепелац.
> Т.е. с одной стороны — бесстыднейшее (и крайне спорное с юридической точки
> зрения) копирование и паразитирование на чужих идеях и наработкахSTMicro им как бы железки не давал - сами совместимые разработали. Почему так нельзя - науке неизвестно. Вроде бы API не есть копирайченая штука, оракла vs гугл на этой теме помнится завернули.
> кому-то это тоже окажется интересным ~открытием или дополнят/поправят (раз уж затронули
> такую интересную мне тему).У узкоглазых есть и еще клоны STM32 от других фирм, разной степени кривизны. Вон там рядом какой-то чудак мыкается, у него оно в бутлоадер не входит чего-то.
> Еще у них есть ответвления F1xx-like которых в оригинале нет - например
> мелкие QFN с USB и общим видом железа как у F1xx.
> У STMicro именно такого комбо почему-то и нет, при всем разнообразии.
> Неужто никто usb не хотел в мелком корпусе c F1xx? Да ну ладно?!Собственно, я об этой ситуации и говорил в «это давно напрашивалось, но ST это посчитали не очень-то нужным, а китайцы взяли и реализовали».
>> кристалл последовательной флеш-памяти, разварив и залив несколько кристаллов в одном корпусе.
> А вы их щупали? Флеху шить программно пробовали? Оно по flash controller
> не совместимо? А то даташит вроде как клон STM-ов 1 в 1.А чего бы ему быть несовместимым? Поскольку общение с флеш-памятью что в оригинале, что тут идёт не напрямую, а через внутренний контроллер, этот самый контроллер прекрасно абстрагирует все подробности. В общем-то, наличие команд для стирание страницами и записи словами не зависит от типа флеш-памяти, это везде есть.
>> Т.е. с одной стороны — бесстыднейшее (и крайне спорное с юридической точки
>> зрения) копирование и паразитирование на чужих идеях и наработках
> STMicro им как бы железки не давал - сами совместимые разработали. Почему
> так нельзя - науке неизвестно. Вроде бы API не есть копирайченая
> штука, оракла vs гугл на этой теме помнится завернули.Насколько я помню, тот же оракл на эту тему ещё долго будет пытаться что-нибудь у кого-нибудь отжать. Тут тоже момент тонкий: во-первых, не очень ясно, насколько сами и с нуля (или, как часто бывает, по знакомству что-то добыли с соседнего завода; если сам ST посчитает их угрозой, наверняка постарается накопать информацию о подобных эпизодах), во-вторых, могут докопаться до похожей маркировки (типа, почти до неразличимости, с торговыми марками и товарными знаками это стандартная практика; не могу сказать точно, насколько это применимо тут), рисунков и фраз из документации, может, какие-то решения по периферии вообще запатентованы. Но, вполне может быть (всё-таки я не юрист), что тут и правда ситуация «а что, так можно было?», т.е. просто кто-то первым понял что ничего не мешает сделать так, а остальные сами себя ограничивали, опасаясь проблем или не считая этот путь перспективным.
> У узкоглазых есть и еще клоны STM32 от других фирм, разной степени кривизны.
> Вон там рядом какой-то чудак мыкается, у него оно в бутлоадер не входит чего-то.А можно подробнее и конкретнее? Интересно, что там ещё бывает из широко доступного.
Для меня большим открытием ещё в своё время стали WCH с их переходниками со всего подряд на всё подряд и самыми дешёвыми МК с аппаратным USB (CH55x), а также Padauk (PDK) с их сверхдешёвыми МК с однократно программируемой памятью (при этом есть ещё и варианты с тем же ядром и нормальной флеш-памятью, но там уже и цена повыше, так что это для отладки больше).
> Собственно, я об этой ситуации и говорил в «это давно напрашивалось, но
> ST это посчитали не очень-то нужным, а китайцы взяли и реализовали».Я честно говоря не понял почему в мелком корпусе, с usb и вообще F103-like обвесом - "не очень нужное". Китайцы вот тоже. Минимум сравнимого что я знаю это F103 в qfn36, но у китайцев и мельче есть, qfn28 чтоли, выводок F150. Что-то ST с маркетингом перемудрил местами, имхо.
> А чего бы ему быть несовместимым? Поскольку общение с флеш-памятью что в
> оригинале, что тут идёт не напрямую, а через внутренний контроллер, этот
> самый контроллер прекрасно абстрагирует все подробности.Ну вот в этом и вопрос был - смогли ли они вывесить аналогичный интерфейс железки. И это вопрос к тому кто реально пробовал этой железкой покомандовать, соответственно :)
> В общем-то, наличие команд для стирание страницами и записи словами не зависит
> от типа флеш-памяти, это везде есть.Просто для SPI это технически дольше и сложнее. Но если железка-посредник оттранслирует интерфейс - почему бы и нет. Я кажется начинаю понимать как это: mem-mapped SPI подпертый кэшом каким-то, так? Узкоглазые вообще любят mmaped spi почему-то в своих чипах.
> Насколько я помню, тот же оракл на эту тему ещё долго будет
> пытаться что-нибудь у кого-нибудь отжать.Пытаться то он может что угодно, но если получится, следующим шагом кто-нибудь запатентует алфавит и мы все дружно залетим за использование этого апи.
> по знакомству что-то добыли с соседнего завода; если сам ST посчитает
> их угрозой, наверняка постарается накопать информацию о подобных эпизодах),1) Вероятно могут и сами что-то разработать.
2) ST тоже не все железки сами разработали, часть у других налицензировали.
3) ST постепенно поразвел зоопарк "HW IP versions" грубо говоря. Да, железо улучшили, но совместимость профакали и дескать используйте наши мегалибы и халы на каких-то мутных лицензиях - "только с чипами stmicro".> А можно подробнее и конкретнее? Интересно, что там ещё бывает из широко доступного.
https://www.opennet.me/openforum/vsluhforumID3/120751.html#153 - где-то вокруг этого. Понятия не имею кто такой CS32, бывают и другие (на остальных фото маркировка нечитаема).
> Для меня большим открытием ещё в своё время стали WCH с их
> переходниками со всего подряд на всё подрядНу мне это уже не особо надо - у меня есть и просто FTDI'ки, а что-то сверх того я и сам фирмвару для мк накорябаю.
> и самыми дешёвыми МК с аппаратным USB (CH55x), а также Padauk (PDK) с их сверхдешёвыми
> МК с однократно программируемой памятьюЯ миллионными тиражами не ворочаю, в иные ниши пристраиваюсь. F1xx мне пришлись по вкусу тем что дешевле какихнить атмег, при том что периферия и ядро сильно круче, а сложность системы... ну, "я в это более-менее врубился" - общий view чипа и чего я с ним делаю и зачем все же сформировался. А вот китайские глюки мне все же ни к чему в вещах для которых мне МК интересны :).
И цена около 1-2 баксов за чип меня не напрягает. А, еще и gcc'ом поддерживается, вплоть до возможности юзануть тулчейн из репов моего линуксного дистра. И stm32flash оттуда же, все-таки удобно.
https://www.sifive.com/boards/hifive1-rev-b
А risc-v сможет достичь сопоставимой производительности?
> А risc-v сможет достичь сопоставимой производительности?RISC-V - это просто открытая система команд. Соответственно, интель может прикрутить декодер RISC-V (RV64IMAFDC) к своим утюгам, и тогда будет RISV-V с сопоставимой производительностью.
P.S. На месте интеля я бы заслал такую фичу инженерам 1-2 года назад (как только спекулятивное исполнение накрылось тазом), и даже наверное начал бы вкладываться в разработку неготовых спецификаций (всё что "Open" в https://en.wikipedia.org/wiki/RISC-V#ISA_base_and_extensions).
> RISC-V - это просто открытая система команд. Соответственно, интель может прикрутить декодер
> RISC-V (RV64IMAFDC) к своим утюгам, и тогда будет RISV-V с сопоставимой производительностью.Кроме этого есть еще и открытые реализации ядер. Это, конечно, не интел - но вообще нормальные 64-битные штуки, для небольших железок с линухом явно хватит.
Risc-v это просто спецификация на набор команд. Вот если вы сделаете хороший быстрый кристалл, то тогда будем вам и сопоставимая производительность. Но, опять же, хорошего кристалла недостаточно -- нужен хороший компилятор. Т.е. такой компилятор, который способен адекватно учесть особенности спецификации и её реализации.
Все как в лучших домах - есть GCC и Clang. И линухом это процессорное ядро поддерживается. И даже некоторые реально существующие SoC.
А потом откопать обратно.
Вот, просто хороший DLS и никакой псевдонаучной претенциозности как у Rust.
DSL
Что такое DLS? Может DSL (Domain Specific Language)?
да хватит играть уже с аббревиатурой LSD
Вообще-то оно на сишечке с асмом.
Ядро на сишечке. Пруф -- нет. Причём пруф раз в 40 больше самого ядра.
> Причём пруф раз в 40 больше самого ядра.А вы чего хотели? Скажите спасибо что он вообще за разумное время обсчитывается.
> Скажите спасибо что он вообще за разумное время обсчитывается.Касперский "при необходимости" посчитает за разумное время любую NP-полную задачу.
> Касперский "при необходимости" посчитает за разумное время любую NP-полную задачу.Он сам как NP-полная задача.
Всего-то пришлось свой компилятор C написать, и потом ещё 200к строк на Isabelle, Haskell и прочих.
В том то и элегантность решения, что компилятор C в 100500 раз проще Раста.
Проще и безопаснее, так как в С нету unsafe
Вот вот, раст настолько убог что написание собственного компилятора С для каждой программы гораздо более элегантное решение чем написание кода на раст
Внезапный поворот: компилятор, которым собирается seL4, написан ни разу не на C!
> Внезапный поворот: компилятор, которым собирается seL4, написан ни разу не на C!Это как-то мешает собрать его компилятором си написаным на си? :)
Слабое приплетание, на троечку.
Давно в области безопасности не было таких хороших вестей
может gnu/hurd кто-нибудь перенесёт на seL4
Ноу проблем. Сколько поатишь?
Флаг в руки, ждём от тебя результатов.
Люди, способные это сделать, не станут заниматься этим "за идею".
Было много попыток перевести Hurd с Mach на L4, к сожалению, все потерпели неудачу.
смысл не в том, чтобы заменить gnu mach на seL4, а в том, чтобы gnu/hurd работал поверх seL4;
иначе говоря, seL4 работает в режиме ядра, а gnu/hurd(gnu mach + translators) в режиме пользователя.
Гурд жестко приколочен к 32 битам. Его теперь проще переписать. Это в вопросу о программистских талантах Столлмана.
На seL4 есть рабочая Genode https://genode.org/ .
Genode под Nova пишется, все остальные ядра для галочки.
что-то не очень заметно, что на платах Arduino используется RISC-V
https://www.sifive.com/boards/hifive1-rev-b
https://shop365481095.world.taobao.com/
https://aliexpress.ru/item/4000299112762.html
Они анонсировали Arduino Cinque и… всё.
Что, впрочем, нисколько не мешает купить другую похожую на Arduino платку с RISC-V.
Скоро ESP RISC-V подъедет
Вот это по настоящему важная новость. Ещё бы понять, как наладить производство устройств на нём.
Берёшь L4 и https://pulp-platform.org// и налаживаешь производство.
Эпл уже решило переходить на RISC-V вместо ARM?
А что, они как-то обсуждали эту возможность?
Я не слышал, но после такой "будоражащей" новости как эта могли и задуматься. Нет.
> Эпл уже решило переходить на RISC-V вместо ARM?Да и черт с ним с эплом. Зато решили WD, Nvidia и много кто еще. При том первая фирма процессоры делает со времен царя гороха.
Интересный исследовательский проект, но преподнесен ради хайпа вокруг RISC-V, который порядком надоел постоянной игрой слов и введением в заблуждение. RISC-V - это лишь открытый набор команд процессора, т.к. открытая спецификация. Сделано это во многом для экспериментов с процессорными архитектурами в университетской среде с целью иметь возможность переиспользовать единый компилятор и набор портированного ПО, не отвлекаясь на всё это от дизайна аппаратура.Автор этой идеи решил коммерциализировать эту идею, так появилась SiFive, являющаяся классической HW IP + design services компанией, такой же как Arm. Их ядра ни разу не открытые и не бесплатные, но да, используют ту самую tools / SW экосистему. По сути, ребятки придумали модель, как за счет open source community решить одну из задач классического HW IP стартапа и быстро оказаться наравне с Arm по размерам экосистемы. Отлично, решили, вот только бизнес всё не взлетает, компания продолжает привлекать внешние инвестиции в развитие и всё больше уходит в design services. Открытость набора команд на качество процессорного ядра, реализующего этот набор, не влияет.
Другие коммерческие RISC-V вендоры почему-то образуются в РФ и Южной Америке. Наверно, потому что пытаются сыграть на волне импортозамещения. Что опять же к реальной технической конкуренции отношения не имеет и к open source процессорному ядру не приближает.
Вообще, идея открытой реализация ядра вызывает один большой вопрос “зачем?”. Ну вот есть оно и что?
Выпустить чип требует далеко не только процессорного ядра, но и других блоков (интерфейсы, памяти и т.п.). Выпустить production ready чип потребует еще и серьезным усилий по дизайну и верификации. Ну и само производство не дешевое удовольствие. Даже есть кто-то выпустил такой чип, в момент изготовления он становится куском кремния, патч на него больше не наложишь.
Еще есть очень крупные продуктовые компании (WD), которые способны сделать свою архитектуру и поддерживать её. Вот они экономят на группе разработки компилятора и отчислениях Arm-у, но почему-то используют эти решения в закрытых системах.
Можно залить в ПЛИС. И это хорошее решение, если заниматься исследованиями процессорных архитектур, но сомнительное, если нужен просто процессор. Xilinx уже предоставляет бесплатное ядро в качестве микроконтроллера, а многие большие FPGA уже содержат Arm A процессор, если нужен мощный embedded CPU.
WD это хорошо (он заменил mips на arm и riscv), но ты забыл про NVIDIA, лет 10 применяющую risc-v в своих видимокартах. Сейчас уже пару лет как есть "десктопы" на risc-v. Особо от x86 не отличаются, но асссемблерных оптимизаций в программах не завезли и поэтому немножко сливает в плане производительности. Цена на порядки адекватней эльбрусов, несмотря на то что в долларах.
Чего лет 10 назад? 10 лет назад архитектура только начала зарождаться.Можно ссылочку на такой десктоп?
Да, внезапно, nvidia стоит у истоков и первая радостно побежала экономить. Насчёт дектопа… Ммм я перепутал с power9, извините.
Вы вообще всё здесь перепутали -- примерно так:>>> Сейчас уже пару лет как есть "десктопы" на risc-v.
Нет.
>>> Особо от x86 не отличаются
Нет!
>>> но асссемблерных оптимизаций в программах не завезли
>>> и поэтому немножко сливает в плане производительности.Нет.
>>> Цена на порядки адекватней эльбрусов, несмотря на то что в долларах.
Нет!
PS: в отличие от Вас -- практик в обсуждаемом вопросе.
Спасибо, я уже признал ошибку. Это было про power9.
risc-v десктоп на power 9
Он risc, это определённо. И он десктоп.
> Интересный исследовательский проект, но преподнесен ради хайпа вокруг RISC-V, который
> порядком надоел постоянной игрой слов и введением в заблуждение. RISC-V -
> это лишь открытый набор команд процессора, т.к. открытая спецификация.
> [...]
>Очень хорошо сформулировано
> Другие коммерческие RISC-V вендоры почему-то образуются в РФ и Южной
> Америке. Наверно, потому что пытаются сыграть на волне импортозамещения.Причём когда минимум из-за одного такого российского безфабричника восторчали уши IBM, у меня лично наметились сомнения, что тут вообще речь про импортозамещение, а не прокорм стратегической лавки кинетического противника в условиях повышенной шагреневости рынков...
Собственно, кто знает всех этих сосновцевых с массухами -- тот и так понимает.
А про кого это вы? Вроде какая-то питерская контора занималась RISK-V
В своё время L4 было прорывом, но поезд несколько продвинулся за >25 лет.Сейчас же уже есть Kaspersky OS, которая принципиально лучше L4 (конечно IMHO, ибо TL;DR):
- тот-же уровень верифицируемости (посредством мат. доказательства) при необходимости.
- различные модели безопасности.
- поддержка POSIX.
- возможность "security by design" для приложений (как сложных наборов компонентов/служб).
- также поддержка жесткого реального времени (пока не из каробки, но обещают).Репутация же L4 оказалась "подмочена" дырявостью продуктов Qualcomm.
Репутацию Kaspersky OS ещё никто не проверял. Да и исходников её не покажут.
Кому нужно уже показали, поэтому и пишу."Проверка" там в основном делается "математикой", поэтому (в сравнении с Linux и тем более вендой) можно узбаготься.
Минусы, которые я пока вижу примерно такие:
- У Евгения (кажется) еще осталась надежда, что их когда-нибудь/может-быть пустят обратно на рынок США и сателлитов. Поэтому продукт подается (IMHO) слишком "глобалистически".
- В разработку вложено очень много (>15 лет), соответственно Евгений не решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.
> не решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.R.I.P
о какой вообще проверке может идти речь при отсутствии открытых исходников?
> > не решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.
> о какой вообще проверке может идти речь при отсутствии открытых исходников?Открыть исходники для проверки - это одно (у M$ в таком режиме они открыты >25 лет).
А перейти на открытую лицензию и модель open source - это совсем другое.Но палка тут о двух концах - если модель (и DSL её описания) окажутся удачными (а похоже так и есть), то повторить уже проверенную концепцию относительно просто поверх любого подходящего ядра (даже натянуть на Linux, хотя будет масса проблем).
Т.е. если Kasperky OS "взлетит" и при этом останется closed-source, то китайцы (или еще кто-то) повторят разработку за ~1-2 года.
>даже натянуть на LinuxТам даже систему виртуальной памяти пофиксить не могут, слишком сложный продукт стал, о какой верификации речь может идти? В лучшем случае миникс верифицируют.
>>даже натянуть на Linux
>Там даже систему виртуальной памяти пофиксить не могут, слишком сложный продукт стал, о какой верификации речь может идти? В лучшем случае миникс верифицируют.Хм, а где в слове "натянуть" есть упоминание верификации ?
> Открыть исходники для проверкиТам хотя бы повторяемость сборки есть? Открыты они.
А если по обновлениям приедет бэкдор например? Какой смысл в открытии "на посмотреть"?
Кода в ОС столько, что найти там все небезопасные вещи очень трудно, даже когда на одни исходники смотришь всем миром. А когда смотрит какая-то одна рабочая группа ограниченное время - это вообще ни о чём...
Не суйтесь вообще с закрытой ОС на рынок. Просто не лезьте. Закрытая ОС - это зло.
>> Открыть исходники для проверки
> Там хотя бы повторяемость сборки есть? Открыты они.
> А если по обновлениям приедет бэкдор например? Какой смысл в открытии "на
> посмотреть"?
> Кода в ОС столько, что найти там все небезопасные вещи очень трудно,
> даже когда на одни исходники смотришь всем миром. А когда смотрит
> какая-то одна рабочая группа ограниченное время - это вообще ни о
> чём...
> Не суйтесь вообще с закрытой ОС на рынок. Просто не лезьте. Закрытая
> ОС - это зло.Рассуждая не зная предмета, вы просто рекламируете свою некомпетентность.
Никого не волнует твоя компетентность. Удел закрытой ОС - два с половиной закрытых роутера.Щас нам Касперский будет про безопасность рассказывать. С бэкдорами прямо от ФСБ, ага.
> Никого не волнует твоя компетентность. Удел закрытой ОС - два с половиной
> закрытых роутера.
> Щас нам Касперский будет про безопасность рассказывать. С бэкдорами прямо от ФСБ,
> ага.Никому не интересно ваше "ихпёртное" мнение (не читал, но осуждаю) без базовой осведомленности об обсуждаемом предмете.
Всегда кто-то "лает" и хейтит, а караван идёт (и с Эльбрусами, и с Альтом и т.д. и т.п. также).
Адью, мосье́.
Да пусть идет, мне вообще пофиг
> Никому не интересно ваше "ихпёртное" мнение (не читал, но осуждаю) без базовой
> осведомленности об обсуждаемом предмете.Ихпертное мнение о структуре управления каспера можно на хабре почитать. Дальше каждый для себя сделает выводы сам.
Ничего себе, вы экспертное сообщество привели!!!
С таким же успехом можно и лукоморье упоминать.
> Ничего себе, вы экспертное сообщество привели!!!Нормальное сообщество айтишников. Получше многих других, имхо. Хоть и хипстерское малость.
> С таким же успехом можно и лукоморье упоминать.
А эти просто правда российской жизни в сатирическом и колоритном изложении.
Хз на счёт управления, не сведущ в вопросе, но видится мне, США не зря и не просто так это счастье выперли.
>>>Кому нужно уже показалимне это всегда нравилось. "у нас есть такие приборы но мы вам их не покажем".
>>>- В разработку вложено очень много (>15 лет)
извиняюсь, os/360 меньше времени строили.
она за эти 15 лет реальное практическое применение хоть где-то нашла? или только "где надо, там и нашла"?
если нет, то это n-ый вариант hurd.
> > В разработку вложено очень много (>15 лет)
> извиняюсь, os/360 меньше времени строили.Считаем что стоили и выбросили, или что z/OS всё еще строят (~60 лет)?
Тем не менее, в любом случае - Ну и что?
> > Кому нужно уже показали
> мне это всегда нравилось. "у нас есть такие приборы но мы вам
> их не покажем".
>
> она за эти 15 лет реальное практическое применение хоть где-то нашла? или
> только "где надо, там и нашла"?
> если нет, то это n-ый вариант hurd.Рассуждая не зная предмета, вы просто рекламируете свою некомпетентность.
z/os в продуктиве работает все эти годы.kasperskyos в продуктиве где-то работает?
лет пять назад в россии рекламировали kasperskyos на крафтвеях. только что зашел на их сайт посмотреть, что как - сетевое "доверенное оборудование" с красивыми сертификатами почему-то на линуксе. как так?
>>>Рассуждая не зная предмета, вы просто рекламируете свою некомпетентность.
кто мешает вам рассудить со знанием? ну правда, вот я спросил, и еще повторюсь, мне не жалко:
kasperskyos в продуктиве где-то работает?
вы уж просветите нас, темных, если не сложно. я волшебное слово знаю: "Пожалуйста!"
> kasperskyos в продуктиве где-то работает?Ну RTFM ведь.
https://os.kaspersky.ru/projects/> вы уж просветите нас, темных, если не сложно. я волшебное слово знаю:
> "Пожалуйста!"На здоровье!
> - В разработку вложено очень много (>15 лет), соответственно Евгений не
> решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.Это по счастью будут в основном его проблемы, да нескольких "везунчиков" которым это добровольно-принудительно втулили. А то что мелкий проприетарщик да еще с орками в управлении переиграет весь остальной мир - так не бывает.
>> - В разработку вложено очень много (>15 лет), соответственно Евгений не
>> решается (и возможно никогда не решится) сделать Kaspersky OS Open Source.
> Это по счастью будут в основном его проблемы, да нескольких "везунчиков" которым
> это добровольно-принудительно втулили.Демагогия и FUD.
> А то что мелкий проприетарщик да еще с
> орками в управлении переиграет весь остальной мир - так не бывает.1. "мелкий", "орки" - А я верно предполагаю что в вашей системе координат Макс является представителем "крупных эльфов" и реикарнацией Тони Старка ;)
2. "так не бывает" - ага, ни разу не было и вот опять ;)
> Демагогия и FUD.Оценка наиболее вероятного развития событий. Такое счастье можно поюзать только если орк машет саблей и грозит отрезать голову.
> 1. "мелкий", "орки" - А я верно предполагаю что в вашей системе координат
Орки сами себя так назвали. Подробности этой истории можно найти на хабре...
Что значит -- "переиграет весь мир"? "Весь мир" и так себя самого переигрывает. Безо всякой помощи. ИТ -- такой, какой он сейчас -- должен умереть.
> Что значит -- "переиграет весь мир"?Это реверанс в адрес "если Kasperky OS "взлетит"". Блин, скорее пингвины научатся летать. Стоп, "given enough rocket power penguins can fly" (c) :D
> Кому нужно уже показали, поэтому и пишу.«Танк шибко секретный! Учёные могут и не знать!» ©
>Кому нужно уже показали, поэтому и пишу.От того, что показали майору, нам не легче.
> при необходимостиОЙ КАК ТОЛСТО...
> > при необходимости
> ОЙ КАК ТОЛСТО...Видимо стоит уточнить для местных ихпёртов, которые (УВЫ) не читали, но осуждают.
Логика ядра верифицирована, но в реальных применениях это мало что даёт (смотрим на факапы Qualcomm и т.п.):
- без верификации всех "ассемблерных вставок" при использовании на конкретной платформе.
- без верификации логики служб и приложений (с учетом взаимодействия и средств контроля ОС).Соответственно, "при необходимости" - относилось к верификации примитивов (связанных с "посадкой" ОС на какую-то конкретную платформу) и к верификации приложений.
TL;DR
Kaspersky OS предлагает контроль взаимодействия отдельных компонентов (служб, приложений) как с ядром, так и между собой - это принципиальное отличие от L4.
Грубо говоря, принципы безопасности/надежности L4 распространяются с ядра на все приложения, службы и систему в целом.
Я всерьёз не могу это воспринимать даже. Закрытое чудо, которое никто не видел, а если даже откроют - то исходники не откроют. Но оно мегабезопасное. "Не имеющее аналогов в мире". Да ну нафиг.Примерно на уровне QP ОС.
L4 лучше хотя бы тем, что она реальна, а не иллюзорна.
> Я всерьёз не могу это воспринимать даже. Закрытое чудо, которое никто не
> видел, а если даже откроют - то исходники не откроют. Но
> оно мегабезопасное. "Не имеющее аналогов в мире". Да ну нафиг.Т.е. если вы не трогали луну руками, то её нет?
Тем не менее, эту "луну" можно потрогать https://os.kaspersky.ru/development/
(если руки растут из нужного места).
Там есть исходный код ядра и его можно собрать и запустить со своими правками?
> Там есть исходный код ядра и его можно собрать и запустить со
> своими правками?Нет.
Но за подробностями лучше RTFM.
> Т.е. если вы не трогали луну руками, то её нет?Разве это не принципиальный вопрос верификации?
> Тем не менее, эту "луну" можно потрогать https://os.kaspersky.ru/development/
И что там дают? Уже собранную игрушку для написания хелловорлдов? Плюс "прямое согласие на сбор и обработку моих данных"
Как там грится? Джентльменамм верят на слово! И тут мне карта как поперла, как поперла!
Как будто репутация у вирусописателей Касперского чем-то сильно лучше Qualcomm.
Касперский и репутация? Хотя, может в каких-то там своих кругах.
Дефачка из PR-отдела отчаянно минусует, размазывая тушь соплями.
> Дефачка из PR-отдела отчаянно минусует, размазывая тушь соплями.Ну не у каждой "дефачке" хватит соплей на вашу чушь ;)
Ты смотри, а девачкам понравилось. Плюсуют. Бедненькие труженицы "IT-сектора".
Всё что я понял, что есть некая шайтан архитектура - RISC, есть её спецификации, есть "разработчики" этих спецификаций и даже есть микропроцессоры. Все открытые процессоры это RISC, не RISC я не нашел.
разработчик спецификация архитектуры Реализации архитектуры
MIPS Technologies, Inc. MIPS
OpenPOWER POWER
университет Беркли RISC-V
OpenCores RISC OpenRISC
OpenSPARC
Sun Microsystem SPARC UltraSPARC T1, UltraSPARC T2
Texas Instruments SPARCv8 LEON2
Fujitsu SPARCv9 SPARC64
Simply RISC SPARC V9 S1 Core
Ну... Спарку можно сразу выкинуть.
Почему?
Теперь есть 15 конкурирующих стандартов.
Что в этом плохого?
А ты подумай... Интел закрыт, как чёрт, жрёт, как слон, и ему абсолютно пох на каких-то 15 открытых "конкурентов" с суперпуперэкономным ядром.
Если бы не было 15 шт, было бы лучше, хуже? Появится ещё 100500, пускай, если взлетит одна и хорошо.
Нет, НЕ хорошо. Это - всего лишь показатель того, что отрасль так до сих пор и находится в состоянии "не знаю, кто там, в яме, но сыр - точно очень любит". И речь здесь - совершенно - не о многовариантности получения одного и того же результата. Да! И, желательно, Тьюринга, лишний раз не поминать...
> абсолютно пох на каких-то 15 открытых "конкурентов" с суперпуперэкономным ядром.Ща им эппл подкатит годный сюрпризец кажись.
УжЕ - нет. И - никто, в ближайшие лет 30 - не подкатит. Не до того будет.
SuperH тоже risc. И amd64 тоже risc, но это тщательно пытаются маскировать. RISC-V эта такая современная альтернатива мипсу (который тоже открыли и закопали, а ведь хорошая альтернатива арму была). В первую очередь стоит вопрос энергоэффективности и возможности свободно дизайнить кастомные чипы без космических откатов. В чём смысл сабжа я затрудняюсь ответить.
Какая из реализаций лучше всего подойдет для ПК, ноутов, планшетов, телефонов?
> Какая из реализаций лучше всего подойдет для ПК, ноутов, планшетов, телефонов?Давно известно - волшебная.
>Давно известно - волшебная.Подозреваю что ирония сарказм.
> amd64 тоже riscНет. А то, что там RISC -- не называется AMD64.
Скорее всего там технология аналогичная тому, что разрабатывала transmeta. Дитя ежа с ужом и эмуляция класических интерфейсов для взаимодействия.
> И amd64 тоже risc, но это тщательно пытаются маскировать.Никто ничего не маскирует. CISC это микрокод выполняющийся поверх RISC ядра. Всегда, даже в 8080.
Ваш Кэп.
Возможно и так. Когда-то я интересовался этим вопросом (когда писал 16 битные программы) и видел утверждения, что cisc в процессорах интел когда-то всё же был. Примерно с P6 всё пошло в разнос, тогда же появились все эти уязвимые бранч предикторы и всё остальное. Они были уязвимыми ещё 20 лет назад, мельдаун и спектра эксплуатируют давным давно известные архитектурные "особенности".
бранч предикторы - следствие наличия конвейера, а никак не микрокода. RISC/CISC тут не при чем.
Но я не вижу тут противоречий. Ведь x86 процессоры (в частности нынешние) архитектурно являются RISC, что я изночально и утверждал.
> Ведь x86 процессоры (в частности нынешние) архитектурно являются RISCЭто тавтология. ВООБЩЕ ВСЕ CISC процессоры архитектурно содержат в себе RISC процессор как ядро.
нет, это как раз ошибка. Вся разница в том кто решает как правильно загружать конвеер и кэши - в risc этим преимущественно занимается компилятор, в cisc внутренняя логика со всеми своими branch prediction, в экстремальной vliw только компилятор. Поэтому собственно risc начались с mips архитектуры, хотя например pdp-11 по системе комманд тоже к ним относят.
RISC-и тоже умеют в макрокомманды или как они называются, когда один опкод заменяется последовательностью других, так что и они могут подвергнуться атакам на тайминг, хоть и теоретически.
> Поэтому собственно risc начались с mips архитектуры, хотя например pdp-11 по системе комманд тоже к ним относят.PDP-11 не относят к RISC только по тому что во времена расcыпухи такого деления не было. Сделай кто сейчас совместимую однокристалку и она станет RISC-ом. Просто мне трудно представить зачем приделывать микрокод к процессору с ортогональной системой команд.
https://ru.wikipedia.org/wiki/%D0%9A1801%D0&#...
Да, я знаю про это. Даже к друзьям на БуКашке периодически ходил играться "для расширения кругозора", сам обладая Спектрумом. Но официально RISC-ом он, как и MOS6502 не называется по той причине, что само понятие в широкие массы было введено только в 90-е.
У меня вообще есть предположение, что слово RISC присваивают процессору, когда хотят громко произнести: "Мы избавились от микрокода чтобы получить одну команду за такт" и избегают когда нужно сказать что "Мы избавились от микрокода чтобы сэкономить на транзисторах"
Нет. У PDP-11 пачка омских режимов адресации, RISC всегда load/store.
> Нет. У PDP-11 пачка омских режимов адресации, RISC всегда load/store.load/store - это вторичный половой признак. Он является следствием, а не причиной и по этому не может считаться в отрыве от других признаков.
На то что является первичным, позволю себе сослаться на автора понятия RISC Джона Кока [1]:
This was the key realization: Imposing microcode between a computer and its users imposes an expensive overhead in performing the most frequently executed instructions. Thus, a key task in designing the experimental machine was to investigate the consequences of exposing a microcomputer directly to the end user. In many cases, a microcomputer limited to instructions executable in one cycle would execute a macro-instruction in about as many cycles as a System/370 Model 168 executing the equivalent instruction. The great potential was that simple instructions would run substantially faster for the same circuit family and cycle time because the overhead of executing a CISC (Complex Instruction-Set Computer) interpreter was pared away.
Он однозначно говорит что RISC получился из CISC удалением микрокода и его интерпретатора. Ортогональность, load/store и прочее - только следствия.
[1] The evolution of RISC technology at IBM: https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=5389855
> по тому
> по этомуДа сколько ж можно?!
>хотя например pdp-11 по системе комманд тоже к ним относят.А что, разве в системе команд PDP11 не было команд, производящих изменения данных прямо в ячейках памяти?
VLIW (EPIC) разве не могут притворяться CISC? Вроде и эльбрусы VLIW, притворяющийся CISC.
> VLIW (EPIC) разве не могут притворяться CISC? Вроде и эльбрусы VLIW, притворяющийся CISC.CISC - это архитектура, а не система команд, а притворяются EPIC-и начиная с Крузо именно поддержкой x86-х команд. И для последних вполне можно сделать и настоящий RISC-процессор, только кому это надо? С такой-то бессистемицей в опкодах.
> Это тавтология. ВООБЩЕ ВСЕ CISC процессоры архитектурно содержат в себе RISC процессор как ядро.Там вон в новости про очередные дыры в интеле разрисовано что оно содержит. RISC это разве что с очень большой натяжкой совы на глобус.
> Всегда, даже в 8080.Ну ты фантазёр…
> Ну ты фантазёр…Люблю опеннет за наличие икспердов. Люди уже даже эмулятор для микрокода 8080 написали, но местное сообщество все-равно говорит что его не существует: https://github.com/jdryg/8080Emu
Наличие микрокода не обязывает ядро быть RISCовым
> Наличие микрокода не обязывает ядро быть RISCовымВозможно он пытается сказать что "блоки выполнения" за uCode ROM сами по себе смахивают на RISC? До некоторой степени, пожалуй, смахивают.
> Возможно он пытается сказать что "блоки выполнения" за uCode ROM сами по себе смахивают на RISC? До некоторой степени, пожалуй, смахивают.Бинго! Первый тезка который это понял. А то что у этих "блоков выполнения" вместо номеров операций и регистров в системе команд используются номера SELECT-ов к логическим блокам, это просто так удобней для CISC.
> Всегда, даже в 8080.Чиво??? RISC ядро появилось в 486
Если не Pentium II
>RISC-V эта такая современная альтернатива мипсу (который тоже открыли и закопали, а ведь хорошая альтернатива арму была).MIPS это спецификация RISC от MIPS Technologies, Inc.
RISC-V это спецификация RISC от RISC Foundation.
Какая из них лучше, хуже?
Вообще мне нравятся SPARC, почему бы их не производить - UltraSPARC T1, UltraSPARC T2?
> Вообще мне нравятся SPARC, почему бы их не производить - UltraSPARC T1, UltraSPARC T2?Так производите. Даже какое-то из ядер выкладывали. Просто это огроменный чип и это будет большое, мучительное и дорогое приключение, а отбить затраты продажами этого... сможете?
Пацаны это то самое открытое железо о котором мечтают все ГНУтые?
нет, это только открытая система комманд без слишком явной привязки к какому-то производителю. Открывать реализацию железа оно не обязывает.
К тому же этих спецификаций вагон и маленькая тележка, я выше писал.
Главное чтобы было всё без лицензионных отчислений.
С виду - без, как начнёшь делать в железе - сразу появятся и отчисления. и патенты, и ещё много чего.
О хо-хо, хо-хо! :(
it is proved to be bug-free relative to a specification
То есть, это всего-лишь доказательство что реализация соответствует спецификации безо всяких этих ваших багов. Это не гарантирует отсутствие багов в спецификации (недавние новости какбэ намекае) и не гарантирует отсутствие уязвимостей в самой архитектуре, которые, при наличии присутствия, превратят весь этот ваш матан в пшик, как мы наблюдаем уже второй год с x86
Две банки жидкого азота господину! Да, можно математически доказать, что проц будет правильно складывать 2+2 и помещать результат в пользовательский регистр, но что будет побочно делать в рабочих буферах...
За науку я готов выпить хоть яду. Проставляйся.
Это не пить... это для твоего проца :)
Мой проц справляется даже без радиатора. Я давно уже не покупаю печки.
>о полном соответствии заданным на формальном языке спецификациям.Пусть сначала докажут что в самих спецификациях нет бага или бэкдора. Для этого нужны спецификации спецификаций. А на них спецификации спецификаций спецификаций. И так до тех пор, пока спецификации спецификаций .... спецификаций не превратятся во что-то простое, где каждому будет очевидно, что нет бага или бэкдора.
Лучшее доказательство - отсутствие спекуляция при работе с памятью.
> Лучшее доказательство - отсутствие спекуляция при работе с памятью.Rowhammer'у так например это похрен.
А вы - точно понимаете значение употребляемых вами слов?
Это, увы, не достижимо в принципе. Ну так Рассель, Кантор, Гедоль ну и НамеНаме считают.
https://github.com/seL4/seL4/blob/master/src/smp/lock.c 25 строк.clh_lock_t big_kernel_lock ALIGN(L1_CACHE_LINE_SIZE);
Да тут не только математически, но и астрально картами Таро можно обосновать.
А тем временем даже в Falcon 9 уже обыденный x86.
Нет. Не обыденный. Не обольщайтесь ложной простотой вопроса.
В Еврефайтерах и Рафалях тоже х86 (купленные на барахолке), а в Ф-22 960-тые и 860-тые.
Отличная новость, и ОС интересная.... Зато попиарили забесплатно закрытую нех от касперыча, чо.
>... Зато попиарили забесплатно закрытую нех от касперыча, чо.Макса Чиркова деньги не интересуют.
> ... Зато попиарили забесплатно закрытую нех от касперыча, чо."Какая страна, такая и ОС".
По итогу самым безопасным окажется ядро "Hello world".