Update license description and move into this repo (#172)

Licensing was previously described on
<https://sel4.systems/Info/license.pml>, but only linked-to from the
docs site. Additionally, the description there was a bit sparse and old.

Signed-off-by: Gerwin Klein <[email protected]>

Signed-off-by: Gerwin Klein <[email protected]>

GettingStarted.md

@@ -14,7 +14,7 @@ This page is a quick start for working with seL4 and its ecosystem.
 ### Sources
 
 Code and proofs are available on [GitHub](https://github.com/seL4), under standard
-[open-source licenses](http://sel4.systems/Info/GettingStarted/license.pml).
+[open-source licenses](/processes/licenses).
 
 There are [many repositories](/MaintainedRepositories).
 Of the most significant are:

_data/sidebar.yml

@@ -37,6 +37,8 @@ toc:
         url: /processes/conduct.html
       - page: Contributing
         url: /processes/contributing.html
+      - page: Licensing
+        url: /processes/licenses.html
       - page: Style Guide
         url: /processes/style-guide.html
       - page: Git Conventions

processes/licenses.md

@@ -0,0 +1,42 @@
+---
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
+---
+
+# Licensing
+
+The code and documentation in the repositories of the [seL4 GitHub
+organisation][seL4-org] are available under standard open-source licenses,
+identified by [SPDX license tags][SPDX].
+
+The seL4 Foundation licenses and accepts contributions for
+
+- the seL4 kernel itself under [GPL Version 2][GPL-2.0-only],
+- user code and proof libraries under the [BSD 2 Clause license][BSD-2-Clause],
+- code and proofs that depend on GPL-code or GPL-proofs under GPL,
+- documentation under [Creative Commons Attribution-ShareAlike][CC-BY-SA-4.0].
+
+Note that, as in the [Linux syscall note for the GPL][GPL-note], the seL4 kernel
+GPL license does *not* cover user-level code that uses kernel services by normal
+system calls - this is merely considered normal use of the kernel, and does
+*not* fall under the heading of "derived work". Syscall headers are provided
+under BSD.
+
+For a longer explanation of how the seL4 license does or does not affect your
+own code see also [this blog post][license-blog].
+
+The repositories of the seL4 GitHub organisation also contain third-party code
+under additional compatible open source licenses. See the individual file
+headers for details, or use one of the publicly available [SPDX] tools to
+generate a software bill of materials. The directory `LICENSES/` in each repository
+contains the text for all licenses that are mentioned by files in that
+repository.
+
+
+[seL4-org]: https://github.com/seL4/
+[GPL-2.0-only]: https://spdx.org/licenses/GPL-2.0-only.html
+[BSD-2-Clause]: https://spdx.org/licenses/BSD-2-Clause.html
+[CC-BY-SA-4.0]: https://spdx.org/licenses/CC-BY-SA-4.0.html
+[SPDX]: https://spdx.org
+[GPL-note]: https://spdx.org/licenses/Linux-syscall-note.html
+[license-blog]: https://microkerneldude.wordpress.com/2019/12/09/what-does-sel4s-license-imply/

projects/sel4/frequently-asked-questions.md

@@ -603,7 +603,7 @@ uptake.
 
 The seL4 kernel is released under GPL Version 2. Userland tools and
 libraries are mostly under BSD. See the
-[license page](https://sel4.systems/Info/license.pml) for more details.
+[license page](/processes/licenses) for more details.
 
 ## How do I contribute to seL4?
 See [How to Contribute](/Contributing).