diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 0ae44bd1..bcccfd9e 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -16,7 +16,7 @@ jobs:
     name: Language Spec PDF
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v2
+    - uses: actions/checkout@v4
     - name: Install texlive and pandoc
       run: |
         sudo apt-get update
@@ -31,32 +31,31 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        python-version: [ '2.x', '3.9' ]
+        python-version: [ '3.9', '3.x' ]
       fail-fast: false
     steps:
-    - uses: actions/checkout@v2
-    - uses: actions/setup-python@v2
+    - uses: actions/checkout@v4
+    - uses: actions/setup-python@v5
       with:
         python-version: ${{ matrix.python-version }}
     - name: Install python packages
       run: |
         cd python-capdl-tool
-        pip install -r requirements.txt
-        pip install nose future
+        pip3 install -r requirements.txt
     - name: Run tests
       run: |
         cd python-capdl-tool/tests
-        nosetests --exe
+        PYTHONPATH=../ ./runall.py
 
   capDL-tool:
     name: capDL-tool (ghc)
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v2
+    - uses: actions/checkout@v4
     - run: |
         sudo apt-get update
         sudo apt-get install libxml2-utils
-    - uses: actions/setup-haskell@v1.1.4
+    - uses: haskell/actions/setup@v2
       with:
         enable-stack: true
         stack-setup-ghc: true
diff --git a/capDL-tool/CapDL/MakeModel.hs b/capDL-tool/CapDL/MakeModel.hs
index aad1c4bf..60bf9c39 100644
--- a/capDL-tool/CapDL/MakeModel.hs
+++ b/capDL-tool/CapDL/MakeModel.hs
@@ -479,6 +479,7 @@ objectOf n obj =
         Obj RTReply_T [] [] -> RTReply
         Obj ARMSID_T [] [] -> ARMSID
         Obj ARMCB_T ps [] -> ARMCB (getCBExtraInfo ps)
+        Obj ARMSMC_T [] [] -> ARMSMC
         Obj _ _ (_:_) ->
           error $ "Only untyped caps can have objects as content: " ++
                   n ++ " = " ++ show obj
@@ -603,6 +604,8 @@ validCapPars (Endpoint {}) ps =
     subsetConstrs (removeConstr (Rights undefined) ps) [Badge undefined]
 validCapPars (Notification {}) ps =
     subsetConstrs (removeConstr (Rights undefined) ps) [Badge undefined]
+validCapPars (ARMSMC {}) ps =
+    subsetConstrs ps [Badge undefined]
 validCapPars (TCB {}) ps =
     subsetConstrs ps [Reply, MasterReply] &&
     (not (containsConstr Reply ps) || not (containsConstr MasterReply ps))
@@ -655,6 +658,7 @@ objCapOf containerName obj objRef params =
         ARMIrq {} -> ARMIRQHandlerCap objRef
         ARMSID {} -> ARMSIDCap objRef
         ARMCB {} -> ARMCBCap objRef
+        ARMSMC -> ARMSMCCap objRef (getBadge params)
     else error ("Incorrect params for cap to " ++ printID objRef ++ " in " ++
                 printID containerName ++ "; got " ++ show params)
 
diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs
index 6a2c0af6..c57412d1 100644
--- a/capDL-tool/CapDL/Model.hs
+++ b/capDL-tool/CapDL/Model.hs
@@ -118,6 +118,9 @@ data Cap
         | ARMIRQHandlerCap { capObj :: ObjID }
         | ARMSIDCap        { capObj :: ObjID }
         | ARMCBCap         { capObj :: ObjID }
+        | ARMSMCCap        {
+            capObj :: ObjID,
+            capBadge :: Word }
 
         -- X86 specific caps
         | IOPortsCap {
@@ -209,6 +212,8 @@ data KernelObject a
     | ARMSID
     | ARMCB { bankNumber :: Maybe Word }
 
+    | ARMSMC
+
 -- X86 specific objects
     | IOPorts { ports :: (Word, Word) }
     | IODevice {
@@ -249,6 +254,7 @@ data KOType
     | ARMIrqSlot_T
     | ARMSID_T
     | ARMCB_T
+    | ARMSMC_T
     | ASIDPool_T
     | PT_T
     | PD_T
@@ -414,6 +420,7 @@ objID = capObj
 hasRights :: Cap -> Bool
 hasRights (NotificationCap {})   = True
 hasRights (EndpointCap {})        = True
+hasRights (ARMSMCCap {})          = True
 hasRights (FrameCap {})           = True
 hasRights _                       = False
 
diff --git a/capDL-tool/CapDL/ParserUtils.hs b/capDL-tool/CapDL/ParserUtils.hs
index b67cea62..5ebcfa63 100644
--- a/capDL-tool/CapDL/ParserUtils.hs
+++ b/capDL-tool/CapDL/ParserUtils.hs
@@ -137,6 +137,7 @@ object_type =
     <|> keyw "rtreply" RTReply_T
     <|> keyw "streamid" ARMSID_T
     <|> keyw "contextbank" ARMCB_T
+    <|> keyw "smc" ARMSMC_T
 
 obj_bit_size :: MapParser ObjParam
 obj_bit_size = do
diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs
index b4ff3ca5..4d71ee9b 100644
--- a/capDL-tool/CapDL/PrintC.hs
+++ b/capDL-tool/CapDL/PrintC.hs
@@ -158,6 +158,11 @@ showCap objs (ARMSIDCap id) _ is_orig _ =
 showCap objs (ARMCBCap id) _ is_orig _ =
     "{.type = CDL_CBCap, .obj_id = " ++ showObjID objs id ++ ", .is_orig = " ++ is_orig ++ "}"
 
+showCap objs (ARMSMCCap id badge) _ is_orig _ =
+    "{.type = CDL_SMCCap, .obj_id = " ++ showObjID objs id ++
+    ", .is_orig = " ++ is_orig ++
+    ", .data = { .tag = CDL_CapData_Badge, .badge = " ++ show badge ++ "}}"
+
 showCap objs (PTCap id _) _ is_orig _ =
     "{.type = CDL_PTCap, .obj_id = " ++ showObjID objs id ++
     ", .is_orig = " ++ is_orig ++ "}"
@@ -379,6 +384,7 @@ showObjectFields _ _ (SC info size_bits) _ _ _ =
 showObjectFields _ _ (RTReply {}) _ _ _ = ".type = CDL_RTReply,"
 showObjectFields _ _ (ARMSID {}) _ _ _ = ".type = CDL_SID,"
 showObjectFields _ _ (ARMCB {}) _ _ _ = ".type = CDL_CB,"
+showObjectFields _ _ ARMSMC _ _ _ = ".type = CDL_SMC,"
 showObjectFields _ _ x _ _ _ = assert False $
     "UNSUPPORTED OBJECT TYPE: " ++ show x
 
diff --git a/capDL-tool/CapDL/PrintUtils.hs b/capDL-tool/CapDL/PrintUtils.hs
index 0b2e6e96..b629d75d 100644
--- a/capDL-tool/CapDL/PrintUtils.hs
+++ b/capDL-tool/CapDL/PrintUtils.hs
@@ -215,6 +215,7 @@ prettyObjParams obj = case obj of
     ARMIrq _ trigger target -> text "arm_irq" <+> maybeParensList[prettyARMIRQTrigger trigger, prettyARMIRQTarget target]
     ARMSID {} -> text "streamid"
     ARMCB {} -> text "contextbank"
+    ARMSMC {} -> text "smc"
 
 capParams [] = empty
 capParams xs = parens (hsep $ punctuate comma xs)
@@ -305,6 +306,8 @@ maybeCapParams cap = case cap of
         capParams (maybeBadge badge ++ maybeRights False rights)
     NotificationCap _ badge rights ->
         capParams (maybeBadge badge ++ maybeRights False rights)
+    ARMSMCCap _ badge ->
+        capParams (maybeBadge badge)
     ReplyCap _ -> capParams [text "reply"]
     MasterReplyCap _ -> capParams [text "master_reply"]
     CNodeCap _ guard gsize ->
@@ -335,6 +338,8 @@ sameParams cap1 cap2 =
     ((EndpointCap _ b1 r1), (EndpointCap _ b2 r2)) -> b1 == b2 && r1 == r2
     ((NotificationCap _ b1 r1), (NotificationCap _ b2 r2)) ->
         b1 == b2 && r1 == r2
+    ((ARMSMCCap _ b1), (ARMSMCCap _ b2)) ->
+        b1 == b2
     ((CNodeCap _ g1 gs1), (CNodeCap _ g2 gs2)) ->
         g1 == g2 && gs1 == gs2
     ((FrameCap _ r1 a1 c1 m1), (FrameCap _ r2 a2 c2 m2)) -> r1 == r2 && a1 == a2 && c1 == c2 && m1 == m2
diff --git a/capDL-tool/CapDL/PrintXml.hs b/capDL-tool/CapDL/PrintXml.hs
index 9a079432..ee6c90e9 100644
--- a/capDL-tool/CapDL/PrintXml.hs
+++ b/capDL-tool/CapDL/PrintXml.hs
@@ -119,6 +119,7 @@ showObjectName MSIIrq {} = "MSIIrq"
 showObjectName ARMIrq {} = "ARMIrq"
 showObjectName ARMSID {} = "ARMSID"
 showObjectName ARMCB {} = "ARMCB"
+showObjectName ARMSMC = "ARMSMC"
 
 --
 -- Get a cap's name.
@@ -158,10 +159,12 @@ showCapName RTReplyCap {} = "RTReplyCap"
 showCapName SchedControlCap {} = "SchedControlCap"
 showCapName ARMSIDCap {} = "ARMSIDCap"
 showCapName ARMCBCap {} = "ARMCBCap"
+showCapName ARMSMCCap {} = "ARMSMCCap"
 
 showExtraCapAttributes :: Cap -> [(String, String)]
 showExtraCapAttributes (EndpointCap _ capBadge _) = [("badge", show capBadge)]
 showExtraCapAttributes (NotificationCap _ capBadge _) = [("badge", show capBadge)]
+showExtraCapAttributes (ARMSMCCap _ capBadge) = [("badge", show capBadge)]
 showExtraCapAttributes (CNodeCap _ guard guardSize) =
     [("guard", show guard), ("guardSize", show guardSize)]
 showExtraCapAttributes (FrameCap _ _ _ False _) = [("cached", "False")]
diff --git a/capDL-tool/CapDL/State.hs b/capDL-tool/CapDL/State.hs
index 1e811db0..7da1a830 100644
--- a/capDL-tool/CapDL/State.hs
+++ b/capDL-tool/CapDL/State.hs
@@ -321,6 +321,7 @@ koType (MSIIrq {}) = MSIIrqSlot_T
 koType (ARMIrq {}) = ARMIrqSlot_T
 koType (ARMSID {}) = ARMSID_T
 koType (ARMCB {}) = ARMCB_T
+koType ARMSMC = ARMSMC_T
 
 objAt :: (KernelObject Word -> Bool) -> ObjID -> Model Word -> Bool
 objAt p ref = maybe False p . maybeObject ref
@@ -357,6 +358,7 @@ capTyp (IRQMSIHandlerCap {}) = MSIIrqSlot_T
 capTyp (ARMIRQHandlerCap {}) = ARMIrqSlot_T
 capTyp (ARMSIDCap {}) = ARMSID_T
 capTyp (ARMCBCap {}) = ARMCB_T
+capTyp (ARMSMCCap {}) = ARMSMC_T
 capTyp _ = error "cap has no object"
 
 checkTypAt :: Cap -> Model Word -> ObjID -> Word -> Logger Bool
@@ -406,10 +408,12 @@ validCapArch X86_64 (IOPTCap {}) = True
 validCapArch ARM11 (ARMIOSpaceCap {}) = True
 validCapArch ARM11 (ARMIRQHandlerCap {}) = True
 validCapArch AARCH64 (ARMIRQHandlerCap {}) = True
+validCapArch AARCH64 (ARMIOSpaceCap {}) = True
 validCapArch AARCH64 (PUDCap {}) = True
 validCapArch AARCH64 (PGDCap {}) = True
 validCapArch AARCH64 (ARMSIDCap {}) = True
 validCapArch AARCH64 (ARMCBCap {}) = True
+validCapArch AARCH64 (ARMSMCCap {}) = True
 validCapArch _ _ = False
 
 checkCapArch :: Arch -> Cap -> ObjID -> Word -> Logger Bool
@@ -466,6 +470,8 @@ validObjArch AARCH64 (PUD {}) = True
 validObjArch AARCH64 (PGD {}) = True
 validObjArch AARCH64 (ARMSID {}) = True
 validObjArch AARCH64 (ARMCB {}) = True
+validObjArch AARCH64 (ARMSMC {}) = True
+validObjArch AARCH64 (ARMIODevice {}) = True
 validObjArch _ _ = False
 
 checkObjArch :: Arch -> KernelObject Word -> ObjID -> Logger Bool
diff --git a/capDL-tool/Main.hs b/capDL-tool/Main.hs
index 094a7120..ffe0baca 100644
--- a/capDL-tool/Main.hs
+++ b/capDL-tool/Main.hs
@@ -164,6 +164,7 @@ genObjectSizeMap m =
                       , ("seL4_ARMIRQ",              ARMIrqSlot_T)
                       , ("seL4_ARMSID",              ARMSID_T)
                       , ("seL4_ARMCB",               ARMCB_T)
+                      , ("seL4_ARMSMC",              ARMSMC_T)
                       ]
 
 -- Abort with an error message if 'isFullyAllocated' fails.
diff --git a/capDL-tool/capDL-tool.cabal b/capDL-tool/capDL-tool.cabal
index e664abaa..40341122 100644
--- a/capDL-tool/capDL-tool.cabal
+++ b/capDL-tool/capDL-tool.cabal
@@ -17,8 +17,8 @@ copyright:           Data61, CSIRO
 category:            Development
 build-type:          Simple
 extra-source-files:  README.md
-cabal-version:       >=1.18
-tested-with:         GHC == 8.8.4, GHC == 9.0.2
+cabal-version:       1.18
+tested-with:         GHC == 9.2.8
 
 executable parse-capDL
   main-is:             Main.hs
@@ -32,7 +32,7 @@ executable parse-capDL
   build-depends:
                        -- Included libraries
                        array >=0.5 && <0.6,
-                       base >= 4.13 && <4.16,
+                       base >= 4.16,
                        containers >=0.6 && <0.7,
                        filepath >=1.4 && <1.5,
                        mtl >=2.2 && <2.3,
@@ -40,7 +40,7 @@ executable parse-capDL
                        unix >=2.7 && <3,
 
                        -- Other libraries
-                       base-compat >= 0.11 && <0.12,
+                       base-compat == 0.12.*,
                        lens >= 4.15,
                        MissingH >=1.4 && <1.6,
                        pretty >=1.1 && <1.2,
@@ -59,3 +59,5 @@ executable parse-capDL
 
   ghc-options:         -O2 -Werror -Wall -fno-warn-name-shadowing
                        -fno-warn-missing-signatures -fno-warn-type-defaults
+                       -fno-warn-incomplete-uni-patterns
+                       -fno-warn-incomplete-record-updates
diff --git a/capDL-tool/stack.yaml b/capDL-tool/stack.yaml
index d3af03cd..a8ed73f0 100644
--- a/capDL-tool/stack.yaml
+++ b/capDL-tool/stack.yaml
@@ -4,7 +4,7 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
-# Stackage LTS Haskell 19.12 (ghc-9.0.2)
-resolver: lts-19.12
+# Stackage LTS Haskell 20.25 (ghc-9.2.8)
+resolver: lts-20.25
 
 local-bin-path: .
diff --git a/capdl-loader-app/include/capdl.h b/capdl-loader-app/include/capdl.h
index f6f05855..94e27843 100644
--- a/capdl-loader-app/include/capdl.h
+++ b/capdl-loader-app/include/capdl.h
@@ -83,6 +83,9 @@ typedef enum {
     CDL_ARMIOSpaceCap,
     CDL_SIDCap,
     CDL_CBCap,
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    CDL_SMCCap,
+#endif
 #endif
 #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX)
     CDL_VCPUCap,
@@ -169,8 +172,10 @@ typedef enum {
     CDL_Frame         = seL4_ARM_SmallPageObject,
 #ifdef CONFIG_ARCH_AARCH64
     CDL_PUD           = seL4_ARM_PageUpperDirectoryObject,
+#if !(defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined (CONFIG_ARM_PA_SIZE_BITS_40))
     CDL_PGD           = seL4_ARM_PageGlobalDirectoryObject,
 #endif
+#endif
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
     CDL_VCPU          = seL4_ARM_VCPUObject,
 #endif
@@ -208,6 +213,9 @@ typedef enum {
     CDL_ARMInterrupt = seL4_ObjectTypeCount + 11,
     CDL_SID = seL4_ObjectTypeCount + 12,
     CDL_CB = seL4_ObjectTypeCount + 13,
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    CDL_SMC = seL4_ObjectTypeCount + 14,
+#endif
 #endif
 #ifdef CONFIG_ARCH_RISCV
     CDL_Frame = seL4_RISCV_4K_Page,
diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c
index e2cafec0..617019c5 100644
--- a/capdl-loader-app/src/main.c
+++ b/capdl-loader-app/src/main.c
@@ -663,6 +663,12 @@ unsigned int create_object(CDL_Model *spec, CDL_Object *obj, CDL_ObjID id, seL4_
     }
 #endif
 
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    if (CDL_Obj_Type(obj) == CDL_SMC) {
+        return seL4_NoError;
+    }
+#endif
+
 #if !CONFIG_CAPDL_LOADER_STATIC_ALLOC
     if (isDeviceObject(obj)) {
         seL4_Word paddr = CDL_Obj_Paddr(obj);
@@ -1790,6 +1796,12 @@ static void init_cnode_slot(CDL_Model *spec, init_cnode_mode mode, CDL_ObjID cno
         src_index = seL4_CapASIDControl;
         move_cap = false;
         break;
+#ifdef CONFIG_ALLOW_SMC_CALLS
+    case CDL_SMCCap:
+        src_index = seL4_CapSMC;
+        move_cap = false;
+        break;
+#endif
     default:
         src_index = orig_caps(target_cap_obj);
         break;
@@ -1906,12 +1918,12 @@ static void init_copy_addr(seL4_BootInfo *bi)
      * the next 16mb alignment where we can map in a pagetable.
      */
     uintptr_t bi_start = (uintptr_t)bi;
-    copy_addr = ROUND_UP(bi_start + PAGE_SIZE_4K + bi->extraLen, 0x1000000);
+    copy_addr = ROUND_UP(bi_start + seL4_BootInfoFrameSize + bi->extraLen, 0x1000000);
 }
 
 static void cache_extended_bootinfo_headers(seL4_BootInfo *bi)
 {
-    uintptr_t cur = (uintptr_t)bi + PAGE_SIZE_4K;
+    uintptr_t cur = (uintptr_t)bi + seL4_BootInfoFrameSize;
     uintptr_t end = cur + bi->extraLen;
 
     while (cur < end) {
diff --git a/object_sizes/object_sizes.yaml b/object_sizes/object_sizes.yaml
index bb4443e0..90da4e5c 100644
--- a/object_sizes/object_sizes.yaml
+++ b/object_sizes/object_sizes.yaml
@@ -3,6 +3,7 @@
 #include <autoconf.h>
 #include <sel4/constants.h>
 #include <sel4/sel4_arch/constants.h>
+#include <sel4/sel4_arch/deprecated.h>
 #include <sel4/mode/types.h>
 seL4_TCBObject: seL4_TCBBits
 seL4_EndpointObject: seL4_EndpointBits
@@ -65,3 +66,4 @@ seL4_MSIIRQ: 0
 seL4_ARMIRQ: 0
 seL4_ARMSID: 0
 seL4_ARMCB: 0
+seL4_ARMSMC: 0
diff --git a/python-capdl-tool/capdl/Allocator.py b/python-capdl-tool/capdl/Allocator.py
index 1ce613e8..0b25d0c2 100644
--- a/python-capdl-tool/capdl/Allocator.py
+++ b/python-capdl-tool/capdl/Allocator.py
@@ -19,7 +19,7 @@
     Notification, TCB, Untyped, IOPageTable, Object, IRQ, IOPorts, IODevice, \
     ARMIODevice, VCPU, ASIDPool, SC, SchedControl, RTReply, ObjectType, \
     ObjectRights, IOAPICIRQ, MSIIRQ, IRQControl, get_object_size, ASIDControl, \
-    DomainControl, is_aligned, ARMIRQMode, ARMIRQ, ContextBank, StreamID
+    DomainControl, is_aligned, ARMIRQMode, ARMIRQ, ContextBank, StreamID, SMC
 from capdl.util import ctz
 from .Spec import Spec
 
@@ -168,6 +168,8 @@ def alloc(self, type, name=None, label=None, **kwargs):
             o = StreamID(name)
         elif type == ObjectType.seL4_ARMCB:
             o = ContextBank(name)
+        elif type == ObjectType.seL4_ARMSMC:
+            o = SMC(name)
         else:
             raise Exception('Invalid object type %s' % type)
         self.spec.add_object(o)
diff --git a/python-capdl-tool/capdl/Cap.py b/python-capdl-tool/capdl/Cap.py
index 7ca8d573..89965331 100644
--- a/python-capdl-tool/capdl/Cap.py
+++ b/python-capdl-tool/capdl/Cap.py
@@ -7,7 +7,8 @@
 from __future__ import absolute_import, division, print_function, \
     unicode_literals
 
-from capdl.Object import Object, Frame, CNode, Endpoint, Notification, SchedControl
+from capdl.Object import Object, Frame, CNode, Endpoint, Notification, \
+    SchedControl, SMC
 
 
 class Cap(object):
@@ -48,7 +49,8 @@ def set_guard_size(self, guard_size):
     def set_badge(self, badge):
         # Only endpoint caps can be badged.
         assert isinstance(self.referent, Endpoint) or \
-            isinstance(self.referent, Notification)
+            isinstance(self.referent, Notification) or \
+            isinstance(self.referent, SMC)
         assert badge % 2**28 == badge, 'badges can be a maximum of 28 bits'
         self.badge = badge
 
@@ -85,7 +87,7 @@ def __repr__(self):
             return "sched_control (core: %d)" % self.referent.core
 
         if isinstance(self.referent,
-                      (Frame, Endpoint, Notification)):
+                      (Frame, Endpoint, Notification, SMC)):
             is_frame = isinstance(self.referent, Frame)
             rights = [sym for sym, flag in
                       [('R', self.read),
@@ -101,7 +103,7 @@ def __repr__(self):
         if isinstance(self.referent, Frame) and \
                 self.mapping_container is not None:
             extra.append('mapping: (%s, %d)' % (self.mapping_container.name, self.mapping_slot))
-        if isinstance(self.referent, (Endpoint, Notification)) and \
+        if isinstance(self.referent, (Endpoint, Notification, SMC)) and \
            self.badge is not None:
             extra.append('badge: %d' % self.badge)
         if isinstance(self.referent, CNode):
diff --git a/python-capdl-tool/capdl/ELF.py b/python-capdl-tool/capdl/ELF.py
index 2bb757cf..76579456 100644
--- a/python-capdl-tool/capdl/ELF.py
+++ b/python-capdl-tool/capdl/ELF.py
@@ -149,7 +149,6 @@ def get_pages(self, infer_asid=True, pd=None, use_large_frames=True, addr_space=
         existing_pages = []
         if addr_space:
             # Update symbols with their vaddrs in the AddressSpaceAllocator if we were given one
-            existing_pages = []
             for (symbol, (sizes, caps)) in iteritems(addr_space.get_symbols_and_clear()):
                 assert self.get_symbol_size(symbol) >= sum(sizes), \
                     "Symbol (%s:%d) must have same or greater size than supplied cap range (%d)" % (
diff --git a/python-capdl-tool/capdl/Object.py b/python-capdl-tool/capdl/Object.py
index c159fdce..20371ecd 100644
--- a/python-capdl-tool/capdl/Object.py
+++ b/python-capdl-tool/capdl/Object.py
@@ -96,6 +96,8 @@ class ObjectType(Enum):
     seL4_ARMSID = auto()
     seL4_ARMCB = auto()
 
+    seL4_ARMSMC = auto()
+
     seL4_AARCH64_PGD = auto()
     seL4_AARCH64_PUD = auto()
 
@@ -681,6 +683,17 @@ def get_size_bits(self):
         return None
 
 
+class SMC(Object):
+    def __init__(self, name):
+        super().__init__(name)
+
+    def __repr__(self):
+        return '%s = smc' % self.name
+
+    def get_size_bits(self):
+        return None
+
+
 def is_aligned(value, size_bits):
     """
     Return true if value is aligned to the provided alignment
diff --git a/python-capdl-tool/requirements.txt b/python-capdl-tool/requirements.txt
index aa98d871..4b5fd2db 100644
--- a/python-capdl-tool/requirements.txt
+++ b/python-capdl-tool/requirements.txt
@@ -1,14 +1,14 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 #
 # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 #
 # SPDX-License-Identifier: BSD-2-Clause
 #
 aenum
-orderedset
+ordered-set
 pyelftools
 six
 sortedcontainers
 concurrencytest
 hypothesis
-nose
+future
diff --git a/python-capdl-tool/tests/__init__.py b/python-capdl-tool/tests/__init__.py
index c1f4224e..c2cd0897 100644
--- a/python-capdl-tool/tests/__init__.py
+++ b/python-capdl-tool/tests/__init__.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 #
 # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 #
diff --git a/python-capdl-tool/tests/allocator.py b/python-capdl-tool/tests/allocator.py
index 7b6c08b0..fea85b9c 100644
--- a/python-capdl-tool/tests/allocator.py
+++ b/python-capdl-tool/tests/allocator.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 #
 # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 #
diff --git a/python-capdl-tool/tests/runall.py b/python-capdl-tool/tests/runall.py
index ec42e134..d631dd06 100755
--- a/python-capdl-tool/tests/runall.py
+++ b/python-capdl-tool/tests/runall.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
 #
 # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
diff --git a/python-capdl-tool/tests/testelf.py b/python-capdl-tool/tests/testelf.py
index 0aef76e3..21507228 100755
--- a/python-capdl-tool/tests/testelf.py
+++ b/python-capdl-tool/tests/testelf.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 #
 # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 #
diff --git a/python-capdl-tool/tests/testmerge.py b/python-capdl-tool/tests/testmerge.py
index 209cc943..0dc5c3c0 100755
--- a/python-capdl-tool/tests/testmerge.py
+++ b/python-capdl-tool/tests/testmerge.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 #
 # Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 #