Link alla notizia: https://www.hwupgrade.it/news/sistemi-operativi/google-annuncia-un-nuovo-sistema-operativo-si-chiama-kataos-ed-e-matematicamente-sicuro_111050.html

Un nuovo sistema operativo basato su seL4 e Rust è stato presentato da Google, con l'intento di creare un ambiente privo di molte classi di bug: a dimostrarne l'assenza sono prove matematiche

Click sul link per visualizzare la notizia.

"machine learning ambientale" leggendo questo la parola "sicuro", nel senso di privacy, decade... :-) Rimarrà la sicurezza del codice...

"machine learning ambientale" leggendo questo la parola "sicuro", nel senso di privacy, decade... :-) Rimarrà la sicurezza del codice...
Ma già dalla prima parola del titolo della notizia, la privacy decade...:D

Ma già dalla prima parola del titolo della notizia, la privacy decade...:D

ahah bellissima :D

kata? davvero? le prime due sillabe della parola "catastrofe" in parecchie lingue nel mondo?

Boh....

Sicuro si....fino a quando qualcuno lo bucherà!

Google annuncia un nuovo sistema operativo: si chiama KataOS ed è matematicamente sicuro*

(*) che verrà presto abbandonato.

kata? davvero? le prime due sillabe della parola "catastrofe" in parecchie lingue nel mondo?


È un’abbreviazione, il nome completo è KatastrofOS.

È un’abbreviazione, il nome completo è KatastrofOS.
Sponsorizzato dalla Morlock Motors...
(per pochi, immagino...):D

Ma in che senso matematicamente sicura? E' possibile dimostrare matematicamente l'assenza di bug di programmazione?

@marcowave
se è per questo i kata sono anche uno degli aspetti fondamentali per chi fa arti marziali giapponesi:
https://it.wikipedia.org/wiki/Kata


Detto questo quoto @Popye, è sicuro fino a quando non sarà così appetibile da volersi impegnare a bucarlo!

Ma in che senso matematicamente sicura? E' possibile dimostrare matematicamente l'assenza di bug di programmazione?

Quella è impossibile da fornire, ma è possibile dimostrare che sono assenti alcune classi di bug specifiche: "A formal proof of functional correctness was completed in 2009. The proof provides a guarantee that the kernel's implementation is correct against its specification, and implies that it is free of implementation bugs such as deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialised variables. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified." (Wikipedia (https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4))

Allora vi informo che Kataos e anche il nome di un vino pugliese... mi sa che il produttore vivrà di reddita con i soldi che gli dovrà pagare Google per il nome. :D

Non ho le competenze per dire quanto questo passaggio a Rust renda l'os intrinsecamente più sicuro ma trovo la cosa interessante, inoltre trovo anche più il fatto che sia scritto per girare su RiscV e che Google pubblicherà la documentazione sia lato software che hardware.

Ecco mi sta venendo un dubbio, ma con questa cosa che ognuno si fa la sua cpu e poi ci cuce sopra il software.. non c'è il rischio che porti via via ad una frammentazione massiva del mercato?

kata? davvero? le prime due sillabe della parola "catastrofe" in parecchie lingue nel mondo?
Boh....

Che in greco poi vuol dire "sotto", "giù"... che "cala" insomma... non proprio un'accezione positiva.

Ma in che senso matematicamente sicura? E' possibile dimostrare matematicamente l'assenza di bug di programmazione?

Ci sarà di mezzo TLA+ in tutto ciò.

Ironicamente, tanti progetti che avevano "Kata" nel nome sono falliti miserabilmente.

Matematicamente sicuro che non lo userà nessuno come accade ogni volta che viene presentato un nuovo OS.

Matematicamente sicuro :asd: :asd: :asd:

La Matematica Non è un' opinione :D

Sponsorizzato dalla Morlock Motors...
(per pochi, immagino...):D

:sofico: