ΠœΠΈΠΊΡ€ΠΎΡΠ΄Ρ€ΠΎ seL4 матСматичСски Π²Π΅Ρ€ΠΈΡ„ΠΈΡ†ΠΈΡ€ΠΎΠ²Π°Π½ΠΎ для Π°Ρ€Ρ…ΠΈΡ‚Π΅ΠΊΡ‚ΡƒΡ€Ρ‹ RISC-V

ΠžΡ€Π³Π°Π½ΠΈΠ·Π°Ρ†ΠΈΡ RISC-V Foundation сообщила ΠΎ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠΈ Ρ€Π°Π±ΠΎΡ‚Ρ‹ микроядра seL4 Π½Π° систСмах с Π°Ρ€Ρ…ΠΈΡ‚Π΅ΠΊΡ‚ΡƒΡ€ΠΎΠΉ Π½Π°Π±ΠΎΡ€Π° ΠΊΠΎΠΌΠ°Π½Π΄ RISC-V. ВСрификация сводится ΠΊ матСматичСскому Π΄ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²Ρƒ надёТности Ρ€Π°Π±ΠΎΡ‚Ρ‹ seL4, ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠ΅ ΡΠ²ΠΈΠ΄Π΅Ρ‚Π΅Π»ΡŒΡΡ‚Π²ΡƒΠ΅Ρ‚ ΠΎ ΠΏΠΎΠ»Π½ΠΎΠΌ соотвСтствии Π·Π°Π΄Π°Π½Π½Ρ‹ΠΌ Π½Π° Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΠΎΠΌ языкС спСцификациям. Π”ΠΎΠΊΠ°Π·Π°Ρ‚Π΅Π»ΡŒΡΡ‚Π²ΠΎ надёТности позволяСт ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒ seL4 Π² критичСски Π²Π°ΠΆΠ½Ρ‹Ρ… систСмах Π½Π° Π±Π°Π·Π΅ процСссоров RISC-V RV64, Ρ‚Ρ€Π΅Π±ΡƒΡŽΡ‰ΠΈΡ… ΠΏΠΎΠ²Ρ‹ΡˆΠ΅Π½Π½ΠΎΠ³ΠΎ уровня надёТности ΠΈ Π³Π°Ρ€Π°Π½Ρ‚ΠΈΡ€ΡƒΡŽΡ‰ΠΈΡ… отсутствиС сбоСв. Π Π°Π·Ρ€Π°Π±ΠΎΡ‚Ρ‡ΠΈΠΊΠΈ ПО, Ρ€Π°Π±ΠΎΡ‚Π°ΡŽΡ‰Π΅Π³ΠΎ ΠΏΠΎΠ²Π΅Ρ€Ρ… ядра seL4, ΠΌΠΎΠ³ΡƒΡ‚ Π±Ρ‹Ρ‚ΡŒ ΠΏΠΎΠ»Π½ΠΎΡΡ‚ΡŒΡŽ ΡƒΠ²Π΅Ρ€Π΅Π½Ρ‹, Ρ‡Ρ‚ΠΎ Π² случаС сбоя Π² ΠΎΠ΄Π½ΠΎΠΉ части систСмы, Π΄Π°Π½Π½Ρ‹ΠΉ сбой Π½Π΅ распространится Π½Π° ΠΎΡΡ‚Π°Π»ΡŒΠ½ΡƒΡŽ систСму ΠΈ, Π² частности, Π΅Ρ‘ критичСскиС части.

Π˜Π·Π½Π°Ρ‡Π°Π»ΡŒΠ½ΠΎ микроядро seL4 Π±Ρ‹Π»ΠΎ Π²Π΅Ρ€ΠΈΡ„ΠΈΡ†ΠΈΡ€ΠΎΠ²Π°Π½ΠΎ для 32-разрядных процСссоров ARM, Π° ΠΏΠΎΠ·Π΄Π½Π΅Π΅ для 64-разрядных процСссоров x86. ΠžΡ‚ΠΌΠ΅Ρ‡Π°Π΅Ρ‚ΡΡ, Ρ‡Ρ‚ΠΎ комбинация ΠΎΡ‚ΠΊΡ€Ρ‹Ρ‚ΠΎΠΉ Π°ΠΏΠΏΠ°Ρ€Π°Ρ‚Π½ΠΎΠΉ Π°Ρ€Ρ…ΠΈΡ‚Π΅ΠΊΡ‚ΡƒΡ€Ρ‹ RISC-V с ΠΎΡ‚ΠΊΡ€Ρ‹Ρ‚Ρ‹ΠΌ микроядром seL4 ΠΏΠΎΠ·Π²ΠΎΠ»ΠΈΡ‚ Π΄ΠΎΠ±ΠΈΡ‚ΡŒΡΡ Π½ΠΎΠ²ΠΎΠ³ΠΎ уровня бСзопасности, Ρ‚Π°ΠΊ ΠΊΠ°ΠΊ Π°ΠΏΠΏΠ°Ρ€Π°Ρ‚Π½Ρ‹Π΅ ΡΠΎΡΡ‚Π°Π²Π»ΡΡŽΡ‰ΠΈΠ΅ Π² пСрспСктивС Ρ‚ΠΎΠΆΠ΅ ΠΌΠΎΠ³ΡƒΡ‚ Π±Ρ‹Ρ‚ΡŒ ΠΏΠΎΠ»Π½ΠΎΡΡ‚ΡŒΡŽ Π²Π΅Ρ€ΠΈΡ„ΠΈΡ†ΠΈΡ€ΠΎΠ²Π°Π½Ρ‹, Ρ‡Π΅Π³ΠΎ Π½Π΅Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎ Π΄ΠΎΠ±ΠΈΡ‚ΡŒΡΡ для ΠΏΡ€ΠΎΠΏΡ€ΠΈΠ΅Ρ‚Π°Ρ€Π½Ρ‹Ρ… Π°ΠΏΠΏΠ°Ρ€Π°Ρ‚Π½Ρ‹Ρ… Π°Ρ€Ρ…ΠΈΡ‚Π΅ΠΊΡ‚ΡƒΡ€.

ΠŸΡ€ΠΈ Π²Π΅Ρ€ΠΈΡ„ΠΈΠΊΠ°Ρ†ΠΈΠΈ seL4 прСдполагаСтся, Ρ‡Ρ‚ΠΎ ΠΎΠ±ΠΎΡ€ΡƒΠ΄ΠΎΠ²Π°Π½ΠΈΠ΅ Ρ€Π°Π±ΠΎΡ‚Π°Π΅Ρ‚ ΠΊΠ°ΠΊ заявлСно ΠΈ спСцификация ΠΏΠΎΠ»Π½ΠΎΡΡ‚ΡŒΡŽ описываСт ΠΏΠΎΠ²Π΅Π΄Π΅Π½ΠΈΠ΅ систСмы, Π½ΠΎ Π½Π° Π΄Π΅Π»Π΅ ΠΎΠ±ΠΎΡ€ΡƒΠ΄ΠΎΠ²Π°Π½ΠΈΠ΅ Π½Π΅ ΠΈΠ·Π±Π°Π²Π»Π΅Π½ΠΎ ΠΎΡ‚ ошибок, Ρ‡Ρ‚ΠΎ Ρ…ΠΎΡ€ΠΎΡˆΠΎ дСмонстрируСтся Π²ΡΠΏΠ»Ρ‹Π²Π°ΡŽΡ‰ΠΈΠΌΠΈ рСгулярно ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΠ°ΠΌΠΈ Π² ΠΌΠ΅Ρ…Π°Π½ΠΈΠ·ΠΌΠ΅ спСкулятивного выполнСния инструкций. ΠžΡ‚ΠΊΡ€Ρ‹Ρ‚Ρ‹Π΅ Π°ΠΏΠΏΠ°Ρ€Π°Ρ‚Π½Ρ‹Π΅ ΠΏΠ»Π°Ρ‚Ρ„ΠΎΡ€ΠΌΡ‹ ΡƒΠΏΡ€ΠΎΡ‰Π°ΡŽΡ‚ ΠΈΠ½Ρ‚Π΅Π³Ρ€Π°Ρ†ΠΈΡŽ связанных с Π±Π΅Π·ΠΎΠΏΠ°ΡΠ½ΠΎΡΡ‚ΡŒΡŽ ΠΈΠ·ΠΌΠ΅Π½Π΅Π½ΠΈΠΉ — Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, для блокирования всСх Π²ΠΎΠ·ΠΌΠΎΠΆΠ½Ρ‹Ρ… ΠΊΠ°Π½Π°Π»ΠΎΠ² ΡƒΡ‚Π΅Ρ‡ΠΊΠΈ ΠΏΠΎ сторонним ΠΊΠ°Π½Π°Π»Π°ΠΌ, Π² ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… Π³ΠΎΡ€Π°Π·Π΄ΠΎ эффСктивнСй ΠΈΠ·Π±Π°Π²ΠΈΡ‚ΡŒΡΡ ΠΎΡ‚ ΠΏΡ€ΠΎΠ±Π»Π΅ΠΌΡ‹ Π°ΠΏΠΏΠ°Ρ€Π°Ρ‚Π½ΠΎ, Ρ‡Π΅ΠΌ ΠΏΡ‹Ρ‚Π°Ρ‚ΡŒΡΡ ΠΈΡΠΊΠ°Ρ‚ΡŒ ΠΎΠ±Ρ…ΠΎΠ΄Π½Ρ‹Π΅ ΠΏΡƒΡ‚ΠΈ ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠ½ΠΎ.

Напомним, Ρ‡Ρ‚ΠΎ Π°Ρ…ΠΈΡ‚Π΅ΠΊΡ‚ΡƒΡ€Π° seL4 ΠΏΡ€ΠΈΠΌΠ΅Ρ‡Π°Ρ‚Π΅Π»ΡŒΠ½Π° выносом частСй для управлСния рСсурсами ядра Π² пространство ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚Π΅Π»Ρ ΠΈ примСнСния для Ρ‚Π°ΠΊΠΈΡ… рСсурсов Ρ‚Π΅Ρ… ΠΆΠ΅ срСдств разграничСния доступа, ΠΊΠ°ΠΊ для ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚Π΅Π»ΡŒΡΠΊΠΈΡ… рСсурсов. ΠœΠΈΠΊΡ€ΠΎΡΠ΄Ρ€ΠΎ Π½Π΅ прСдоставляСт Π³ΠΎΡ‚ΠΎΠ²Ρ‹Ρ… высокоуровнСвых абстракций для управлСния Ρ„Π°ΠΉΠ»Π°ΠΌΠΈ, процСссами, сСтСвыми соСдинСниями ΠΈ Ρ‚.ΠΏ., вмСсто этого ΠΎΠ½ΠΎ прСдоставляСт лишь ΠΌΠΈΠ½ΠΈΠΌΠ°Π»ΡŒΠ½Ρ‹Π΅ ΠΌΠ΅Ρ…Π°Π½ΠΈΠ·ΠΌΡ‹ для управлСния доступом ΠΊ физичСскому адрСсному пространству, прСрываниям ΠΈ рСсурсам процСссора. ВысокоуровнСвыС абстракции ΠΈ Π΄Ρ€Π°ΠΉΠ²Π΅Ρ€Ρ‹ для взаимодСйствия с ΠΎΠ±ΠΎΡ€ΡƒΠ΄ΠΎΠ²Π°Π½ΠΈΠ΅ΠΌ Ρ€Π΅Π°Π»ΠΈΠ·ΡƒΡŽΡ‚ΡΡ ΠΎΡ‚Π΄Π΅Π»ΡŒΠ½ΠΎ ΠΏΠΎΠ²Π΅Ρ€Ρ… микроядра Π² Ρ„ΠΎΡ€ΠΌΠ΅ Π·Π°Π΄Π°Ρ‡, выполняСмых Π½Π° ΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚Π΅Π»ΡŒΡΠΊΠΎΠΌ ΡƒΡ€ΠΎΠ²Π½Π΅. Доступ Ρ‚Π°ΠΊΠΈΡ… Π·Π°Π΄Π°Ρ‡ ΠΊ ΠΈΠΌΠ΅ΡŽΡ‰ΠΈΠΌΡΡ Ρƒ микроядра рСсурсам организуСтся Ρ‡Π΅Ρ€Π΅Π· ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½ΠΈΠ΅ ΠΏΡ€Π°Π²ΠΈΠ».

RISC-V прСдоставляСт ΠΎΡ‚ΠΊΡ€Ρ‹Ρ‚ΡƒΡŽ ΠΈ Π³ΠΈΠ±ΠΊΡƒΡŽ систСму ΠΌΠ°ΡˆΠΈΠ½Π½Ρ‹Ρ… инструкций, ΠΏΠΎΠ·Π²ΠΎΠ»ΡΡŽΡ‰ΡƒΡŽ ΡΠΎΠ·Π΄Π°Π²Π°Ρ‚ΡŒ микропроцСссоры для ΠΏΡ€ΠΎΠΈΠ·Π²ΠΎΠ»ΡŒΠ½Ρ‹Ρ… областСй примСнСния, Π½Π΅ трСбуя ΠΏΡ€ΠΈ этом отчислСний ΠΈ Π½Π΅ налагая условий Π½Π° использованиС. RISC-V позволяСт ΡΠΎΠ·Π΄Π°Π²Π°Ρ‚ΡŒ ΠΏΠΎΠ»Π½ΠΎΡΡ‚ΡŒΡŽ ΠΎΡ‚ΠΊΡ€Ρ‹Ρ‚Ρ‹Π΅ SoC ΠΈ процСссоры. Π’ настоящСС врСмя Π½Π° Π±Π°Π·Π΅ спСцификации RISC-V Ρ€Π°Π·Π½Ρ‹ΠΌΠΈ компаниями ΠΈ сообщСствами ΠΏΠΎΠ΄ Ρ€Π°Π·Π»ΠΈΡ‡Π½Ρ‹ΠΌΠΈ свободными лицСнзиями (BSD, MIT, Apache 2.0) развиваСтся нСсколько дСсятков Π²Π°Ρ€ΠΈΠ°Π½Ρ‚ΠΎΠ² ядСр микропроцСссоров, SoC ΠΈ ΡƒΠΆΠ΅ ΠΏΡ€ΠΎΠΈΠ·Π²ΠΎΠ΄ΠΈΠΌΡ‹Ρ… Ρ‡ΠΈΠΏΠΎΠ². ΠŸΠΎΠ΄Π΄Π΅Ρ€ΠΆΠΊΠ° RISC-V присутствуСт начиная с выпусков Glibc 2.27, binutils 2.30, gcc 7 ΠΈ ядра Linux 4.15.

Π˜ΡΡ‚ΠΎΡ‡Π½ΠΈΠΊ: opennet.ru