# Found This On The Internet   :\



## RedPhoenix (Apr 11, 2019)

I can't STAND fanboyism of ANY kind, and this time, it seems to come from an OpenBSD user.   I use both Operating Systems, so Mr. OpenBSD user, give me a break.   FreeBSD rocks.


----------



## RedPhoenix (Apr 11, 2019)

RedPhoenix said:


> I can't STAND fanboyism of ANY kind, and this time, it seems to come from an OpenBSD user.   I use both Operating Systems, so Mr. OpenBSD user, give me a break.   FreeBSD rocks.   View attachment 6363


I also had to use GIMP to edit out a dirty word since this is a public forum.


----------



## rigoletto@ (Apr 11, 2019)

That is well know, come out when the current 'CoC' come out.


----------



## rigoletto@ (Apr 12, 2019)

My gripe with OpenBSD is that "Secure by Default" literature without any mathematical proof of that.


----------



## Deleted member 30996 (Apr 12, 2019)

I object.

The information provided is slanderous and was invalid at the time of writing,

The FreeBSD Code of Conduct was issued Feb 15, 2018.

The claim that FreeBSD has "No exploit mitigation whatsoever" was already proven false as FreeBSD 11.0 RELEASE, which was released October, 2016, had System Hardening Options included in the standard build process.

The claim that is is "So useless that people have to create derivative distributions for it to be useful" opinion only.

FreeBSD doesn't include Xorg in the base install like OpenBSD, which should be considered as far as comparisons of "Secure by Default".

I type this from one of my FreeBSD desktops so it too "works as a desktop OS". I have an OpenBSD desktop as well.


----------



## ralphbsz (Apr 12, 2019)

The claims on both sides of the picture are ludicrously wrong.

But many of the counter-claims in here are also ridiculous.  Security does not just come from mathematical proofs, to begin with.  I know a few OpenBSD developers (sat next to one for a a few months in my job), and they do not believe that everything they do is perfect, nor do they ignore other technologies.


----------



## rigoletto@ (Apr 12, 2019)

Just for the record the seL4 is considered the most secure (open-source) kernel by a large part of the CS researchers, exactly because the whole code was proofed (of the implementation) using Isabelle/HOL (took seven years). Another one heavily prised is Muen (with proofs of no runtime errors), SPARK written.

*[EDIT]*

For the record the FreeBSD DTrace is being formalized by a long time user.


----------



## ralphbsz (Apr 12, 2019)

I know about seL4.  It is a microkernel.  That means it doesn't do most of the things a normal kernel does.  It does not contain a file system, nor a networking stack, nor authentication and rights management, nor hardware abstraction and IO.  It only does virtual memory management (providing an address mapping for processes), process scheduling, and a very simple form of IPC.  Matter-of-fact, the primary author of L4 worked at the same research lab as I did, and before that worked with my best friend from high school when working at the GMD.

I don't want to minimize the accomplishment of those people; being able to prove 10K lines of code to be formally correct is absolutely heroic, and a milestone in that field of research.  But 10K lines of code are not an OS.  Correctness proofs for something as big as a useful general purpose OS (at least for a server or router, even without UI) is still far from possible today.

Similarly, the algorithms from Dijkstra's old book are nice.  In particular it's nice to watch how he reasons about each algorithm, and verifies it as he goes.  Today we do much of the same thing ... the idea of adding checks pre- and post-conditions (a.k.a. "assert") is to some extent an outcome of that book.  But Dijkstra's vision is nowhere near for practical-size programs, except in very specialized environments (trusted computing infrastructure in infosec, and extreme reliability code for things like the space shuttle life support control system).  Very little code is formally verified today (sadly).

And you know, from the standpoint of OpenBSD, FFS as a file system really is good enough.  OpenBSD is not intended to be the next Linux or Windows, it does not want to reach 90% market share, nor does it want to run on high-performance computers.  It is intended to be a small but functional Unix implementation, with full networking and server infrastructure, and a basis for a functioning GUI.  It does that really well, as long as you don't have requirements that are outside the things it wants to do.  If you absolutely need ZFS or something (because you want to build a file server appliance that is protected against undetected disk read errors and has CRC on the data path), don't use OpenBSD.  If you want full scalability to processors with many cores, don't use OpenBSD.  If you have unusual hardware (like I had a newish wireless card I was trying to use an AP), don't use OpenBSD.  But for the things OpenBSD is intended for, FFS does the job, and it's old, well-tested, and reliable.


----------

