Actually you are; you suggested that perhaps QMail and OpenBSD, while not being particularly vulnerable pieces of software, may be being used incorrectly (your confidential email example, as one example of what I'm talking about).
How is this using it incorrectly? Should OpenBSD not be used in instances where users may have access to private information and have some ability to export this information? Should OpenBSD not be used in any situation where an internal user may be malicious or stupid? This really narrows down its use, wouldn't you say?

I think you are somewhat confusing the issue by discussing security from a 1000 ft perspective in the same paragraphs as security from a 10 ft perspective. A lot of people seem to have mistaken your statements as referring to vulnerable software, whereas I do understand you are talking about secure software.
Since I am discussing both validation (security) and verification (vulnerabilities) both are relevant. Unfortunately the two may sometimes be interchangeable.

Consider the trojan example. If OpenBSD had a specification it would state something similar to: "Subjects shall not be granted specific access to a given object unless the permission explicitly (owner) or implicitly (group/world) allow it." In the trojan example, a user is able to access files they did not initially have access to, without the owner intentionally granting them. Is this a security issue? Should the specification have stated that copied and new objects cannot be granted permissions beyond their owner without a formal change management procedure? Or is this a vulnerability issue? The access control system was not robust enough to have prevented this attack?

You could argue the issue either way as either approach would have prevented the specific hole.

The real issue you are trying to put forth here is not anything OpenBSD or QMail have dominion over, and lies wholly under the control of the administrator.
How do you figure? How can an administrator ensure that private documents are only emailed to addresses with the rights to view them? This is specifically a design issue.

If you are simply saying that vulnerability-free software isn't enough to ensure a secure system, well duh, I thought that was obvious.
You'd think this should be obvious... yet the vast, vast majority of security focus is on vulnerabilities. Particularly with the examples of qmail and OpenBSD, just because they have few vulnerabilities they are claimed to be secure.

Quite frequently in my experiences as a developer, I've encountered situations where formal development models fail rather easily. For instance, you get one piece of bad analysis, and an application is broken and probably stays that way until a redesign.
I agree with you here, unfortunately the reasoning behind this is more about the way corporations work and less about how formal models work.
Typically the specification is thrown together by someone who used to be a developer and they were such a good developer that they moved up to the architect/designer level. Unfortunately most of the skills required to be a good developer are not so useful as an architect. I can't tell you how many times I've spoken to engineers from large corporations that have really bizarre specs.

Infact one that I saw recently, the client had a very bizarre spec on the hardware portion of a project. They wanted something like a 120' 3.72" coax cable of some type. (I have no idea how much you know about physics so I'll explain.) A very bad attempt at a poor man's phase matching. They figured if the length of the new cable was the same as the other (of a different type mind you that actually needed to be that long) that the phase would be the same. Unfortunately this isn't true (different dialectrics, etc) and it put the new cable (which only needed to be about 6' long) under the noise floor. On the surface it would seem to have made sense, but not to a person who actually knows how to design such things. Long story short... blame the Peter Principal for your flawed specifications as companies prefer to use their own engineers as architects since "they are already familiar with everything."

Beyond all of this, there are exists several tried, true, and proven security models out there... and if none suit your needs, it has been my experience that a project with a custom formal model laid out by professionals familiar with such things and can develop proof of their model will be a much better and frequently cheaper, product... not to mention having a more predictable development schedule.
A bad model can ruin a project and scar all involved, and that is just plain unfortunate... but when you consider that every model should be expressed as a verifiable equation, there really is no excuse for such mishaps.

cheers,

catch