Live data from Hacker News

OpenBSD 6.0 released

undeadly.org

101–110 of 139 posts

Re: OpenBSD 6.0 released

#101
post #36

Earlier quoted context omitted.

Is a "bound-checking memory-safe C compiler" even possible in the general case without implementing a new Rust-like language?

Yes. But, you typically have to use a theorem prover to build up static checking for functions, and then enforce proof obligations on callers to said functions. If done in a system like Coq or Isabelle, the proof obligations become a parallel markup to C that is used in conjunction with the source code to enforce policies. Bounds checking is one policy -- and a relatively easy one to implement at that -- and other po…

That's not true. You just use a compiler transformation. See this:

https://news.ycombinator.com/item?id=12407156

Difference between memory safety and full, formal verification of correctness. You're describing the latter. Definitely check out Myreen et al's CakeML work, COGENT at NICTA, and AutoCorres/Simpl used in seL4. They might have stuff to speed up your own tool development. I wish you great luck on your project. :)

Re: OpenBSD 6.0 released

#102

Earlier quoted context omitted.

I used OpenBSD CURRENT on the Thinkpad Carbon X1 for 3 months earlier this year, and my experience has been that hardware support is not a problem for a "knowledge worker" (I am assuming you don't need things like HDMI audio for that). The main problem is software that is outdated, unavailable, or buggy on non-Linux platforms. I came crawling back to Linux in the end.

Thanks. Though a knowledge worker sometimes does need to connect their laptop to a TV for collaboration and presentations. > The main problem is software that is outdated, unavailable, or buggy on non-Linux platforms What kinds of applications could you not find a good solution for?

> What kinds of applications could you not find a good solution for?

* LibreOffice Writer (lowriter) had an annoying bug where it would sometimes take over a second to redraw the toolbar buttons, and the editor was unavailable during that time. This happened on save, resize, or unhiding the window.

* Konsole's logic to identify the name of the foreground process would occasionally go into an infinite loop and all the konsole windows would lockup and need to be kill -9'd. It can be avoided by using tmux but that's inconvenient. This is sad because it's the most featureful and user-friendly terminal emulator I know of.

* No good C++ IDEs.

* No support for cargo in the rust packages.

* No workable virtualization.

Also, if you use OpenBSD on a laptop, you'd be crazy not to use GNOME 3 in my opinion. Support for the other DEs are not on par.

Re: OpenBSD 6.0 released

#103

Earlier quoted context omitted.

Thanks. Though a knowledge worker sometimes does need to connect their laptop to a TV for collaboration and presentations. > The main problem is software that is outdated, unavailable, or buggy on non-Linux platforms What kinds of applications could you not find a good solution for?

> What kinds of applications could you not find a good solution for? * LibreOffice Writer (lowriter) had an annoying bug where it would sometimes take over a second to redraw the toolbar buttons, and the editor was unavailable during that time. This happened on save, resize, or unhiding the window. * Konsole's logic to identify the name of the foreground process would occasionally go into an infinite loop and all the…

Thanks for the tips; that's very helpful

> * No workable virtualization.

For those interested, they are working on it AFAIK. Look up vmm/vmd.

Re: OpenBSD 6.0 released

#104

Earlier quoted context omitted.

I've wondered about OpenBSD on the NTC CHIP computer. I have one that I haven't quite gotten around to doing anything with that I'd love to OpenBSD-ify.

It is supported.

Oh, well, that makes things easy then. Do you know off hand which image one uses?

Re: OpenBSD 6.0 released

#105

Earlier quoted context omitted.

Yes. But, you typically have to use a theorem prover to build up static checking for functions, and then enforce proof obligations on callers to said functions. If done in a system like Coq or Isabelle, the proof obligations become a parallel markup to C that is used in conjunction with the source code to enforce policies. Bounds checking is one policy -- and a relatively easy one to implement at that -- and other po…

That's not true. You just use a compiler transformation. See this: https://news.ycombinator.com/item?id=12407156 Difference between memory safety and full, formal verification of correctness. You're describing the latter. Definitely check out Myreen et al's CakeML work, COGENT at NICTA, and AutoCorres/Simpl used in seL4. They might have stuff to speed up your own tool development. I wish you great luck on your projec…

Compiler transformation can solve most of these concerns, but it is not perfect due to undecidability. Compiler transformations will always be conservative, falling back on runtime enforcement.

The main edge cases I've run into -- hence my need for building a tool like this -- is dealing with tight performance concerns found in realtime and embedded applications. Falling back to runtime enforcement is not an option, and neither is trusting developers to be able to fully analyze complex control-flow and data-flow paths without solid tooling.

For general-purpose applications, of course, compiler transformation with runtime fallbacks is perfectly acceptable.

Re: OpenBSD 6.0 released

#106
post #32

Earlier quoted context omitted.

It does? I was under the impression the only reason anyone still did that was to give something physical to donators.

One nice thing about the physical CDs is that they're trustworthy source for the release's signify pubkeys (which you can compare with the ones on the website.)

What if someone tampers the CD before it is delivered to you?

Re: OpenBSD 6.0 released

#107

This is a good opportunity to ask: Can anyone recommend a laptop I could put OpenBSD on and be fully functional for busy workdays (i.e., when I need to spend 100% of the day being a knowledge worker with a reliable tool I don't have to think about, and 0% being a sysadmin trying to get their tool to work)? On one hand I've seen threads on HN and Reddit saying how OpenBSD works flawlessly, esp. on various Thinkpads. O…

I run OpenBSD on a T420s and an X220i without any trouble, but I made very sure to get Intel graphics and WiFi as Nvidia and Broadcom are not supported.

Re: OpenBSD 6.0 released

#108

I'm trying to use the austrian mirror, ftp5.eu.openbsd.org, but I'm getting empty directories or "Permission denied" when trying to access the packages folders http://ftp5.eu.openbsd.org/ftp/pub/OpenBSD/6.0/packages/

Have you tried ftp2? I had problems today with one of them (can't remember which worked and which didn't).

EDIT: http://ftp2.eu.openbsd.org/pub/OpenBSD/

Re: OpenBSD 6.0 released

#109
"...the kern.usermount sysctl is also no more. Administrators who want to let users mount devices will need to configure doas(1) for that task."

For convenient laptop use I prefer allowing my user account to mount USB drives and have that done by mouseclicks in some way.

Antoine Jacoutot's toad package is not in the 6.0 packages collection, but xfce4-mount is, so I assume I can set up the appropriate doas rule for a user and then configure xfce4-mount to ignore the local drive. I shall have a play on Sunday.

Re: OpenBSD 6.0 released

#110
post #77

Earlier quoted context omitted.

I like having separate partitions (or slices) for everything. The guy who introduced me to UNIX did it so he could mount certain filesystems "ro" or "noexec". He also told me that partitioning can help avoid inode exhaustion but I really doubt that is an issue with modern filesystems. I still partition with NetBSD. It just feels right; even if not necessary.

Oh, I partition too, but I do /, /usr, /var, /var/log, /home, /tmp, /opt (yeah, yeah, I know), and then anything server specific (mail, maybe www). I just don't do the /usr/local.

When I set up NetBSD, I create /, /usr, /var. /tmp, and /home. I have never create a /usr/local partition but I can see value in it is you want /usr itself to be read-only.
Post reply on HN