#
c798c20d |
|
27-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
access: Isabelle2020 update Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
#
c34840d0 |
|
05-Jun-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
global: isabelle update_cartouches
|
#
4463e975 |
|
12-Jun-2019 |
Michael McInerney <Michael.McInerney@data61.csiro.au> |
SELFOUR-1198: update proofs for correct restart PC Fixes a case where a thread can go from Running->Inactive->Restart and use a restart PC that is out of date. An out of date restart PC occurs when a thread was transitioned to running after being in a blocked state, but was never scheduled and so did not execute the traps code that updates the restart PC. This also renames relevant register names for consistency across architectures (FaultIP and NextIP).
|
#
1689dd94 |
|
03-Apr-2019 |
Victor Phan <Victor.Phan@data61.csiro.au> |
cleanup arm ainvs: cleanup Abbreviate Hoare triples that do not care about the return value and whose pre and post conditions are the same. x64 ainvs: cleanup ainvs: cleanup x64 ainvs: cleanup drefine: cleanup
|
#
bed48eba |
|
03-Apr-2019 |
Victor Phan <Victor.Phan@data61.csiro.au> |
access-control: update for new definition of set_object
|
#
2735ad42 |
|
16-Nov-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
access: proof cleanup for tro_alt_trans_spec The proof structure still largely follows Thibaut's scheme; this commit merely adds some speedup, style cleanup, and documentation. Unfortunately, the proof state seems to be just large enough that the built-in record update ruleset runs into limitations, and the standard clasimp tactics start to fail on subgoals in an unpredictable way.
|
#
6e2fbbe7 |
|
01-Nov-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
access: improve comments for policy_wellformed and integrity_obj
|
#
5d1525bb |
|
01-Nov-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
access: proof style cleanup (for GrantReply patch) As the title says, this commit introduces general formatting and style cleanup, but only for the parts touched by the recent GrantReply patch.
|
#
6dfe687a |
|
01-Nov-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
access: fix incorrect spec for bound notifications
|
#
86bbe323 |
|
22-May-2018 |
Thibaut Perami <thibaut.perami@data61.csiro.au> |
access: Fix for GrantReply (SELFOUR-6) Integrity and pasRefined are majorly changed The main repercussions are: - 3 new authorities in the policy: Call, Reply, and DeleteDerived - The cdt and the caps state are linked in pasRefined - CDT parentship no longer implies control in certain cases (is_transferable) - CDT parentship now implies DeleteDerived - Introduction of cdt_change_allowed that specifies which slot your are allowed to modify - Integrity for CDT and CDT list use cdt_changes_allowed - Integrity for objects in now expressed as a transitive closure of atomic transition rules
|
#
fd6d4b87 |
|
04-Nov-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
refactor einvs from Refine and Access into AInvs
|
#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
011e0845 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new comment syntax (result of "isabelle update_comments <dirs>")
|
#
a6c11a2b |
|
31-Jul-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
access-control, infoflow: use generic relation for pasDomainAbs This patch generalises the mapping between authority labels and scheduler domains, so that the access-control integrity property still holds when labels are not partitioned into domains. This lets us use the integrity result on systems that don't use the domain scheduler. The information flow proofs still rely on the domain partitioning, hence we add constraints on the label-domain mapping for the info-flow results to hold. Jira VER-945
|
#
3a22487c |
|
24-Nov-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242) Colloquially known as "invert-fastpath". Update verification efforts on ARM for the following seL4 changes: - scheduling decisions done in possibleSwitchTo are moved to the scheduler - possibleSwitchTo only checks whether the candidate is valid for a fast switch, not its priority, accepting possible candidates immmediately as a switch-to scheduler action - the scheduler checks the candidate against the current thread and against the bitmaps before making a decision - attemptSwitchTo and switchIfRequiredTo are gone - scheduler is now more complicated, and numerous proofs related to it are rewritten from scratch - fast path now checks ready queues via the scheduler bitmaps - L2 scheduler bitmap order reversed for better cache locality Many iterations between the kernel and verification teams were needed to get this right.
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
41d4aa4f |
|
25-Oct-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: update references to renamed constants and facts
|
#
1289f7bc |
|
09-Nov-2016 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Updating remaining proofs for tcb_arch reserved_irq and arch_fault changes * tcb_context rephrasing to (tcb_context o tcb_arch) and respectively for set operations * unfolding of reserved_irq for trivially solving most lemmas * Changes to the inductive definition of integrity_obj to account for tcb_arch and tcb_context new location * Changes to the tcb examples in ExampleSystem to include tcb_arch * Rephrasing of domain_sep_inv to accommodate the ReservedIRQ case * Mostly rephrasing of tcb_context to (some form of) (tcb_context o tcb_arch) * Trivial unfolding of handle_reserved_irq for hoare rules * Examples in Example_Valid_State.thy were updated * Nothing remarkable, mostly rephrasing of tcb_context and ReservedIRQ handling * Fun fact, some proofs are now shorter tags: [VER-623][SELFOUR-413]
|
#
a2d707d1 |
|
14-Aug-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
SELFOUR-553: update rpidrurw in TCBConfigure for simpler Infoflow proofs.
|
#
a96346e3 |
|
26-May-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
SELFOUR-444: Finished InfoFlow and DRefine.
|
#
411af12e |
|
23-May-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
SELFOUR-444: Logic generalised; Access finished. Tweak AInvs proof for Untyped to be more reusable, finish integrity proofs.
|
#
8d4a8eb2 |
|
21-Sep-2016 |
Xin,Gao <xin.gao@nicta.com.au> |
SELFOUR-421: fix coding style
|
#
252ce8df |
|
09-Aug-2016 |
Xin,Gao <xin.gao@nicta.com.au> |
SELFOUR-421: infoflow and infoflow_c builds
|
#
328846ee |
|
04-Jul-2016 |
Xin,Gao <xin.gao@nicta.com.au> |
SELFOUR-421: crefine builds
|
#
0e5ffd1e |
|
27-Apr-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: requalify abstract theories
|
#
14f75701 |
|
21-Apr-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: Access checking
|
#
6f6c5816 |
|
09-Feb-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
SELFOUR-56: Remove diminish rights from IPC
|
#
bc73b112 |
|
04-Feb-2016 |
Gao Xin <xin.gao@nicta.com.au> |
l4v-sabre: change type of irq to be 10 word
|
#
7aaa8ed7 |
|
25-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: Access and InfoFlow now build
|
#
457a55a8 |
|
01-Nov-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
add arch_tcb object to C, rename aep -> ntfn
|
#
d88a931e |
|
01-Sep-2015 |
Ramana Kumar <Ramana.Kumar@nicta.com.au> |
history squashed patch for aep-binding
|
#
d7e874c8 |
|
30-Jun-2015 |
Matthew Fernandez <matthew.fernandez@nicta.com.au> |
Access: Fix trivial comment typo.
|
#
177e5bf1 |
|
06-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
2015 update for access
|
#
71e7dcc3 |
|
13-Aug-2014 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Fix Access, InfoFlow and DRefine.
|
#
fc6e5771 |
|
10-Aug-2014 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Proof updates, working as far as AInvs.
|
#
1af1d2b6 |
|
08-Aug-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
some of the global Isabelle2014 renames option_case -> case_option sum_case -> case_sum prod_case -> case_prod Option.set -> set_option Option.map -> map_option option_rel -> rel_option list_all2_def -> list_all2_iff map.simps -> list.map tl.simps -> list.sel(2-3) the.simps -> option.sel
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|