Open indolering opened 2 years ago
Sidenote: criticizing formally verified works for a lack of complete specs is shortsighted. When seL4 first came out, everyone complained that the verification didn't extend to the binary ... then they went ahead and proved it down to the binary. There are plenty of valid critiques of seL4, but the limitations of formal verification isn't one of them. Formal verification is just a means to achieving high-assurance code.
Contribution is welcomed!
Contribution is welcomed!
Where is the source file for the Architecture Specification document?
Architecture Specification document is clearly outdated and honestly it would need to be written from scratch. @marmarek @andrewdavidwong I know there were some post a while ago about this architecture document but where should we update some of this part like @indolering is suggesting?
For seL4-specific stuff we might want to check with the seL4 developers, to make sure what we include is accurate.
For seL4-specific stuff we might want to check with the seL4 developers, to make sure what we include is accurate.
What are you wanting to leave in? I think it would be enough to cut the shade and start out the section by supporting the use of a high assurance hypervisor when it's available for use on commodity systems (see also: SeKVM).
Since the original architecture document was written 10+ years ago and probably as a word processing document of some kind, maybe it should just be re-written in qubes-doc? Still, it would be helpful if the original document can be found (as PDF generally removes a lot of formatting).
Architecture Specification document is clearly outdated and honestly it would need to be written from scratch. @marmarek @andrewdavidwong I know there were some post a while ago about this architecture document but where should we update some of this part like @indolering is suggesting?
I also vaguely remember that discussion, but I can't find it now. I have no idea where the source code/file of the arch-spec doc is. I've never had access to it, AFAIK, as it was before my time.
Since the original architecture document was written 10+ years ago and probably as a word processing document of some kind, maybe it should just be re-written in qubes-doc?
That would probably be best.
Since I was unable to find an existing issue for updating the arch-spec doc, I suppose I'll generalize this issue.
There seem to be efforts underway to create a Qubes-like system on the basis of seL4 - possibly using parts of Qubes. See Suggested Projects | seL4 docs and Makatea: Qubes-like OS on seL4 | TS - Trustworthy Systems. It might be interesting to get in contact with the developers.
I was in contact with them recently and the conclusion was that while seL4 should be able to handle everything needed, the userland needs a lot of work.
While using seL4 in Qubes might be a noble goal, this issue is simply about rewriting the arch-spec document, not about changing the architecture of Qubes itself. It's fine if we want to delay rewriting the doc in the expectation that the architecture might change soon, but whenever it gets rewritten, it should accurately reflect the architecture at that time.
Hello, I'm volunteering to convert the PDF to markdown to integrate it in the docs. I'll start by using a PDF to markdown converter and correct glitches. Questions :
Now, time to start !
I think this document deserves separate git repository, it should be standalone thing. While some topics may indeed be already covered in documentation, the document should contain complete description, even if that means duplicating the content (if anything, the reference should go the other way around - docs referring to architecture description for details). In practice, those have different target audience (docs for users, architecture for developers and researchers), so it's unlikely much duplication will happen.
Images: most are likely outdated. Anyway, we don't have sources of them anymore. You can use just placeholders.
I think the starting point should be indeed converting PDF to markdown, then add "outdated" notice to all the sections. Then we can start revising it, which I think is a task for me specifically, to be sure it is accurate. But I'd appreciate help with the initial conversion.
Ok, initial conversion done, I'm editing it now as per the doc guidelines (headers, etc) and to see if nothing's missing/inaccurate compared to the PDF, and following your remarks. Is the markdown version of github the same as the one used on the Qubes docs or discourse ? I'm editing it here for now, so you can see the first initial conversion in my repo.
Is the markdown version of github the same as the one used on the Qubes docs or discourse ?
Short answer: github flavor is fine. In practice, the PDF version will be built using pandoc, so that's what should work.
Ok, last question, hard wrap at 80 chars like the docs, or I leave like it is ? Because the doc is written with a hard-wrapping which seems adapted for PDF/A4 display, and it's been conserved by the conversion.
Yes, lets keep it this way.
I think this document deserves separate git repository, it should be standalone thing. While some topics may indeed be already covered in documentation, the document should contain complete description, even if that means duplicating the content (if anything, the reference should go the other way around - docs referring to architecture description for details). In practice, those have different target audience (docs for users, architecture for developers and researchers), so it's unlikely much duplication will happen.
Well, the docs aren't just for users. After all, we also have a whole category of developer documentation, which is most likely where any duplication would occur. However, I agree that it would be fine to link from the developer documentation to the new arch spec doc (when it's ready) when doing any future deduplication.
Ok, last question, hard wrap at 80 chars like the docs, or I leave like it is ? Because the doc is written with a hard-wrapping which seems adapted for PDF/A4 display, and it's been conserved by the conversion.
Generally speaking, source formatting should be independent of display formatting. In other words, whether the source file text is hard wrapped at 80 should not determine the line wrapping in the resultant PDF. (This is how LaTeX works and how our docs work.) But, in this case, it probably depends on Pandoc and how exactly Pandoc is being used. For example, it's conceivable that your automatic conversion could have inserted Markdown source line breaks (double spaces at the ends of lines), which would cause lines breaks in the resultant PDF in the same locations.
Well, I'm a plaintext guy so PDF, LaTeX, Pandoc, I admit I have no clue how they really work under the hood ! ^^ I'll go along the requirements. No double spaces inserted at the end of lines, only LFs. I asked about wrapping because I copied some random paragraphs from the PDF into a text editor to check the wrapping, LFs after around 100-115 chars. You can check in my repo, the doc is at the root of the fork, "arch-spec-0.3.md". The first commit is the initial import directly from the online converter, the others show my edits and where I stopped. I put comments in the commits notes if needed. Btw, not really important, but tell me if I should use markdown (HTML tags) or Pandoc syntax for superscript (ie < sup >x< /sup > OR ^x^), as it's used by the footnotes and their references.
- Where should I create the new document in the tree : path + filename ?
Since Marek wants this in its own Git repo, I guess it wouldn't have a qubes-doc path or filename. Marek, how are you envisioning we would host, serve, and link to this content? Would the separate Git repo be just for managing the source used to generate a PDF, which is then stored in qubes-attachment?
Btw, not really important, but tell me if I should use markdown (HTML tags) or Pandoc syntax for superscript (ie < sup >x< /sup > OR ^x^), as it's used by the footnotes and their references.
HTML isn't truly part of Markdown; it's just permitted to embed HTML in Markdown. I think either way is fine. We don't really have a good way to do superscripts in qubes-doc. We usually just use HTML.
We usually just use HTML
Ah, I sticked to the pandoc style as I started like that, and I find it smoother on the eye when reading in plaintext, but it's easy to replace (in posix regex, SRC: \^\([0-9][0-9]?\)\^
RPLC: <sup>\1</sup>
, adapt to your flavor).
Is it urgent btw ? Because I'm editing while reading the doc, to understand Qubes, so it's slow. If urgent/ASAP, I'll edit the whole doc at once, no prob. Btw, excellent read so far, it should be the base for a "beginner's guide", with less details ofc.
We usually just use HTML
Ah, I sticked to the pandoc style as I started like that, and I find it smoother on the eye when reading in plaintext, but it's easy to replace (in posix regex, SRC:
\^\([0-9][0-9]?\)\^
RPLC:<sup>\1</sup>
, adapt to your flavor).Is it urgent btw ? Because I'm editing while reading the doc, to understand Qubes, so it's slow. If urgent/ASAP, I'll edit the whole doc at once, no prob.
Like I said, either way is fine. 🙂
Yep, must the important matter was urgency there ^^ Anyway, not an issue now, I've finished the convertion ! As per marek's request, I didn't change any content, except typos. How would you get the doc ? Direct copy/paste from my repo (it's at the root of the fork) or should I pull ?
Since Marek wants this in its own Git repo, I guess it wouldn't have a qubes-doc path or filename. Marek, how are you envisioning we would host, serve, and link to this content? Would the separate Git repo be just for managing the source used to generate a PDF, which is then stored in qubes-attachment?
@marmarek, any thoughts on this?
How would you get the doc ? Direct copy/paste from my repo (it's at the root of the fork) or should I pull ?
Since @marmarek wants it in its own separate repo, which AFAIK doesn't exist yet, I don't think there is any place for you to copy/paste it to or any repo for you to open a PR against yet.
Since Marek wants this in its own Git repo, I guess it wouldn't have a qubes-doc path or filename. Marek, how are you envisioning we would host, serve, and link to this content? Would the separate Git repo be just for managing the source used to generate a PDF, which is then stored in qubes-attachment?
Yes, exactly.
I've created https://github.com/QubesOS/qubes-architecture repository for it. I imagine there should be a script to generate PDF out of md, similar to https://github.com/QubesOS/qubes-offline-doc (but much simpler, since it's about a single document, not a whole set of them).
Ok, wanted to PR against "qubes-architecture" but I can't fork it as the repo is empty ^^ I found some commands to PR to a different repo, but as I'm not a regular github user, don't want to mess things up in qubes public repos ! Maybe the easier would be to create a dummy doc in "qubes-arch" so I can fork then PR ?
@zithro https://github.com/QubesOS/qubes-architecture I've pushed a commit on that. You may be able to fork and contribute now :)
@fepitre, thanks ! I've added the doc and created the PR.
Oh my, I'm such a github noob ... I was wondering why the PR didn't appear in Qubes-arch repo, it's because I did the PR to ... my own repo ! Sorry ...
This is done on the real repo now, but it failed with "policy/qubesos/code-signing - Unable to verify (no valid key found)". I didn't know I needed a signing key for updating the documentation. "doc/code-signing" is not mentionned on "doc/how-to-edit-the-documentation". Should I follow "doc/code-signing" and re-submit ?
This is done on the real repo now, but it failed with "policy/qubesos/code-signing - Unable to verify (no valid key found)". I didn't know I needed a signing key for updating the documentation. "doc/code-signing" is not mentionned on "doc/how-to-edit-the-documentation". Should I follow "doc/code-signing" and re-submit ?
That's because "doc/how-to-edit-the-documentation" only applies to the official website repo and its submodules (in particular, the official documentation repo), whereas qubes-architecture is a brand new repo that @marmarek created just for the purpose of this issue. You don't need a signing key to update qubes-doc. Normally, the "policy/qubesos/code-signing" thing applies mainly to source code repos, not the website or qubes-doc. However, it's up to @marmarek which policies he wants to use for this new repo.
Hello, just realized the doc is still not on the new repo.
@andrewdavidwong ?
I don't have permissions to merge PRs in that repo. (And, even if I did, I'm not sure if I should.) So, I think this is probably a question for @marmarek.
For reference, this seems to be @zithro's PR: https://github.com/QubesOS/qubes-architecture/pull/1
Sorry to insist that much, but I'd like to edit some other docs and I can't because :
As I'm a github noob, and to not pollute this issue, should I rather ask for help on the Qubes forum to resolve this situation ? If you want to contact me directly, I have the same username here and on the forum.
Also I've seen the doc has been deleted from the "qubes-doc" repo. So, don't be afraid to tell me I did that for nothing ! I learnt much about Qubes editing the doc (and think this doc is very useful and should be the base for a new one, including the new features, but w/e !).
As I'm a github noob, and to not pollute this issue, should I rather ask for help on the Qubes forum to resolve this situation ?
Yes, good idea. Also, if you just need general Git help, you are more likely to find it in a non-Qubes-specific venue where there are more knowledgeable Git people around.
Also I've seen the doc has been deleted from the "qubes-doc" repo.
Not sure, but it was probably just deleted because it was too out-of-date and causing problems. That doesn't necessarily mean that a good, up-to-date version won't be added back to qubes-doc.
The FAQ and Architecture Specification document contains outdated information regarding seL4 (such as the lack of support for IOMMU/VT-d) but there is no obvious source file for the the Architecture Specification document in Github. At a minimum, the section should be updated but I think it should removed entirely.
Most of the critique boils down to the seL4 specifications being incomplete, lack of support for commodity hardware, and misc missing functionality. Similar complaints could be lodged about Qubes running so much in
dom0
or the lack of GPU acceleration within AppVMs. But these limitations are the result of anemic funding, not indicators of the quality or feasibility of either project.Qubes would be more secure if it had a formally verified hypervisor and the conclusion states as much. But seL4 provides hypervisor level isolation between individual processes, which could be leveraged to achieve even finer grained levels of compartmentalization. Both projects are driving towards a similar overall architecture of compartmentalized servers, they just have different starting points.
I suspect this section exists because Qubes was initially seeking funding around the time that seL4 was announced. Whatever the reason for its initial inclusion, this section reflects poorly on the Qubes project and should be re-framed or removed.