#
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>")
|
#
166af9e5 |
|
01-Aug-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
access, infoflow: cleanup from previous commit; some style cleanup
|
#
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
|
#
2d0baab4 |
|
13-Mar-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
Proof update for crunch changes
|
#
0f38e200 |
|
25-Feb-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Many proof repairs.
|
#
652cbb96 |
|
14-Mar-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Initial proof updates for combinator changes.
|
#
84633ccb |
|
26-Feb-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
ARM access: proof update for user_context refactor
|
#
2a1beffa |
|
26-Nov-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm: update for simple_ko getter/setter
|
#
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
|
#
b17a3293 |
|
19-May-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm access: ARM Access now builds on arm-hyp
|
#
f86763af |
|
13-Mar-2017 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: new invariant syntax "f {|P|}" Precedence chosen between bind and equality such that f >>= g {P} = foo {Q} works as expected.
|
#
b2f2034b |
|
21-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
Bisim / Access / InfoFlow: updates for Hypervisor stub
|
#
3dafec7d |
|
25-Jan-2017 |
Joel Beeren <Joel.Beeren@nicta.com.au> |
backport changes to ARM proofs from X64 work in progress - replace ARM-specific constants and types with aliases which can be instantiated separately for each architecture. - expand lib with lemmas used in X64 proofs. - simplify some proofs. Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
|
#
979e341d |
|
17-Jan-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: fix ARM build after merge
|
#
47119bf4 |
|
13-Jan-2017 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
wp_cleanup: update proofs for new wp behaviour The things that usually go wrong: - wp fall through: add +, e.g. apply (wp select_wp) -> apply (wp select_wp)+ - precondition: you can remove most hoare_pre, but wpc still needs it, and sometimes the wp instance relies on being able to fit a rule to the current non-schematic precondition. In that case, use "including no_pre" to switch off the automatic hoare_pre application. - very rarely there is a schematic postcondition that interferes with the new trivial cleanup rules, because the rest of the script assumes some specific state afterwards (shouldn't happen in a reasonable proof, but not all proofs are reasonable..). In that case, (wp_once ...)+ should emulate the old behaviour precisely.
|
#
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]
|
#
d7450607 |
|
21-Nov-2016 |
Xin,Gao <xin.gao@nicta.com.au> |
SELFOUR-553: rebase and fix styles and comments
|
#
a2d707d1 |
|
14-Aug-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
SELFOUR-553: update rpidrurw in TCBConfigure for simpler Infoflow proofs.
|
#
2553371a |
|
06-Nov-2016 |
Joel Beeren <joel.beeren@nicta.com.au> |
SELFOUR-64: Remove general Recycle operation This removes the RecycleCap CNodeInvocation, whilst retaining recycle behaviour for Endpoints -- now renamed CNodeCancelBadgedSends.
|
#
ff7ca60d |
|
09-Nov-2016 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
ADT: add kernel entry/exit constraints on domain time left These changes to the automatons are required by: SELFOUR-242: invert bitfield scheduler and optimise fast path Details: When we enter the kernel, the domain time left (ksDomainTime) is never zero. If we entered on a timer interrupt, we may decrement it to zero before the scheduler runs. If we do so, we set the scheduler state to choose_new_thread. When choosing a new thread, the scheduler switches to a new domain if the present one is required, and sets the new domain time left from domain_list (ksDomSchedule). When entering the kernel on a non-interrupt event, we never touch the domain time left, which trivially preserves the new constraints. To prove these, we had to ban a transition from kernel entry to kernel being preempted when handling an interrupt event in InfoFlow. This is fine, as by design handling interrupts is not meant to be preempted by interrupts.
|
#
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.
|
#
a3714e81 |
|
03-Oct-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
SELFOUR-276: Finish proofs for maximum controlled priority (MCP) To finish the proof of refinement to C, the specification for checkPrio needed strengthening: the checkPrio spec now takes a machine word argument. In the spec, priorities are still stored as 8-bit quantities, however. Once the spec was strenthened, it was possible to remove some redundant checks and mask operations from the C code. A thread's maximum controlled priority (MCP) determines the maximum thread priority or MCP it can assign to another thread (or itself).
|
#
252ce8df |
|
09-Aug-2016 |
Xin,Gao <xin.gao@nicta.com.au> |
SELFOUR-421: infoflow and infoflow_c builds
|
#
eb7f7b15 |
|
29-Jun-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arch-split: Tcb_AI.thy done
|
#
d50e43d7 |
|
03-Jul-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: invariants: split CNodeInv_AI [VER-573]
|
#
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
|
#
d7fd8872 |
|
08-Feb-2016 |
Sophie Taylor <sophie.taylor@nicta.com.au> |
SELFOUR-420: Verification of maxIRQ check in handle_interrupt.
|
#
5ede1923 |
|
27-Jan-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
port Access proofs to Isabelle2016-RC2
|
#
ac632c5a |
|
10-Nov-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Wait -> Recv: update proofs
|
#
457a55a8 |
|
01-Nov-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
add arch_tcb object to C, rename aep -> ntfn
|
#
7c3a06a8 |
|
28-Oct-2015 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Minor adjustments caused by Strengthen changes.
|
#
d6f7579b |
|
15-Oct-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
poll: Added new syscall for polling async endpoints (non-blocking wait)
|
#
d88a931e |
|
01-Sep-2015 |
Ramana Kumar <Ramana.Kumar@nicta.com.au> |
history squashed patch for aep-binding
|
#
3372cd32 |
|
15-Jul-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
SELFOUR-220: When calling handleWait, only delete the TCB's ReplyCap when actually waiting on a synchronous endpoint.
|
#
12fa8686 |
|
16-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
fewer warnings
|
#
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.
|
#
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
|
#
50dda770 |
|
22-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
comment cleanup
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|