Go Back   DaemonForums > OpenBSD > OpenBSD General

OpenBSD General Other questions regarding OpenBSD which do not fit in any of the categories below.

Thread Tools Display Modes
Prev Previous Post   Next Post Next
  #1   (View Single Post)  
Old 10th January 2017
psypro psypro is offline
Shell Scout
Join Date: Mar 2016
Location: Continent:Europe
Posts: 124
Default OpenBSD code and mathematical proofs

OpenBSD and proven secure

"I want to point out that "provably secure" has a specific definition which refers to formal verification through the use of mathematical proofs" https://www.quora.com/Can-computer-p...rovably-secure

a) Should OpenBSD base program take aim to be written in such a manner that they can be mathematically proven, like seL4?

b) If so is C the language for the further for OpenBSD, or are more complex compilers/languages like Rust needed to improve code correction to a level where it can be mathematically somewhat proven?

I am no dev. Just want to learn.
Reply With Quote

Thread Tools
Display Modes

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is On
HTML code is Off

Forum Jump

Similar Threads
Thread Thread Starter Forum Replies Last Post
Does OpenBSD use libarchive sandboxing code? betweendayandnight OpenBSD Security 4 13th August 2016 06:46 PM
Google Summer of Code - OpenBSD shep News 9 14th September 2014 07:44 PM
New Open DRM code for OpenBSD shep News 0 22nd March 2013 02:32 AM
*** Error code 1 building OpenBSD 5.1-stable from source comet--berkeley OpenBSD Installation and Upgrading 12 19th May 2012 02:18 AM
Compiling OpenBSD code WeakSauceIII OpenBSD General 4 19th May 2008 12:59 AM

All times are GMT. The time now is 03:33 AM.

Powered by vBulletin® Version 3.8.4
Copyright ©2000 - 2018, Jelsoft Enterprises Ltd.
Content copyright © 2007-2010, the authors
Daemon image copyright ©1988, Marshall Kirk McKusick