{"id":108407,"date":"2023-05-07T00:48:15","date_gmt":"2023-05-06T22:48:15","guid":{"rendered":"https:\/\/prohoster.info\/?p=108407"},"modified":"2023-05-09T08:51:41","modified_gmt":"2023-05-09T06:51:41","slug":"proektu-sel4-prisuzhdena-premiya-acm-software-system-award","status":"publish","type":"post","link":"https:\/\/prohoster.info\/it\/blog\/novosti-interneta\/proektu-sel4-prisuzhdena-premiya-acm-software-system-award","title":{"rendered":"Il progetto seL4 ha ricevuto il premio ACM Software System Award","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Il progetto che sviluppa il microkernel open source seL4 ha ricevuto il premio ACM Software System Award, assegnato annualmente dall'Associazione per l'Informativa Computazionale (ACM), l'organizzazione internazionale pi\u00f9 autorevole nel campo dei sistemi informatici. Il premio \u00e8 stato conferito per i risultati ottenuti nella dimostrazione matematica della affidabilit\u00e0 operativa, che attesta la completa conformit\u00e0 alle specifiche definite in linguaggio formale e riconosce la prontezza all'uso in applicazioni critiche. Il progetto seL4 ha dimostrato che \u00e8 possibile effettuare una verifica formale completa di affidabilit\u00e0 e sicurezza per progetti di livello sistemi operativi industriali, ottenendo questo senza compromettere le prestazioni e la versatilit\u00e0. <\/p>\n
Il premio ACM Software System Award viene assegnato ogni anno per lo sviluppo di sistemi software che hanno avuto un impatto significativo nel settore, introducendo nuove concetti o rivelando nuove aree di applicazione commerciale. L'ammontare del premio \u00e8 di 35.000 dollari statunitensi. Negli anni passati, i premi ACM sono stati conferiti ai progetti GCC e LLVM, e ai loro fondatori Richard Stallman e Chris Lattner. Il premio ha inoltre riconosciuto progetti e tecnologie come UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl\/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ed Eclipse. <\/p>\n
L'architettura del microkernel seL4 \u00e8 notevole per l'allocazione delle parti di gestione delle risorse del kernel nello spazio utente, utilizzando gli stessi strumenti di separazione degli accessi per tali risorse come per le risorse utente. Il microkernel non offre astrazioni di alto livello pronte per la gestione di file, processi, connessioni di rete, ecc.; al contrario, fornisce solo meccanismi minimi per la gestione dell'accesso allo spazio di indirizzamento fisico, alle interruzioni e alle risorse della CPU. Le astrazioni di alto livello e i driver per l'interazione con l'hardware vengono implementati separatamente sopra il microkernel in forma di task eseguiti a livello utente. L'accesso di tali task alle risorse disponibili del microkernel \u00e8 organizzato attraverso la definizione di regole. \n Fonte: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"